We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
erw
colimit.ι_pre
1 parent 4a5c1fd commit 5313444Copy full SHA for 5313444
Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -891,8 +891,7 @@ def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
891
892
@[reassoc (attr := simp)]
893
theorem colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) := by
894
- erw [IsColimit.fac]
895
- rfl
+ simp [colimit.pre]
896
897
898
theorem colimit.ι_inv_pre [IsIso (pre F E)] (k : K) :
0 commit comments