We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
erw
colimit.ι_post
1 parent 97b7e47 commit 9878970Copy full SHA for 9878970
Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -948,8 +948,7 @@ def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
948
@[reassoc (attr := simp)]
949
theorem colimit.ι_post (j : J) :
950
colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) := by
951
- erw [IsColimit.fac]
952
- rfl
+ simp [colimit.post]
953
954
@[simp]
955
theorem colimit.post_desc (c : Cocone F) :
0 commit comments