Commit 2026-09-15 15:38 cf09269b

feat(Tactic/CategoryTheory): map attribute (#37183) Adding @[map] to a lemma named H of shape ∀ .., f = g, where f and g are morphisms in some category C, creates a new lemma named H_map of the form ∀ .. {D} (func : C ⥤ D), F.map f = F.map g and then applies simp only [Functor.map_comp, Functor.map_id].