feat(category_theory/limits): cleanup equalizers (#5214)

golf and make simp more powerful

Author: b-mehta

src/category_theory/limits/shapes/equalizers.lean

@@ -30,8 +30,8 @@ Each of these has a dual.
 ## Main statements
 
 * `equalizer.ι_mono` states that every equalizer map is a monomorphism
-* `is_iso_limit_cone_parallel_pair_of_self` states that the identity on the domain of `f` is an equalizer
-  of `f` and `f`.
+* `is_iso_limit_cone_parallel_pair_of_self` states that the identity on the domain of `f` is an
+  equalizer of `f` and `f`.
 
 ## Implementation notes
 As with the other special shapes in the limits library, all the definitions here are given as
@@ -138,6 +138,19 @@ abbreviation cofork (f g : X ⟶ Y) := cocone (parallel_pair f g)
 
 variables {f g : X ⟶ Y}
 
+/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms `t.π.app zero : t.X ⟶ X`
+    and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is interesting, and we give it the
+    shorter name `fork.ι t`. -/
+abbreviation fork.ι (t : fork f g) := t.π.app zero
+
+/-- A cofork `t` on the parallel_pair `f g : X ⟶ Y` consists of two morphisms
+    `t.ι.app zero : X ⟶ t.X` and `t.ι.app one : Y ⟶ t.X`. Of these, only the second one is
+    interesting, and we give it the shorter name `cofork.π t`. -/
+abbreviation cofork.π (t : cofork f g) := t.ι.app one
+
+@[simp] lemma fork.ι_eq_app_zero (t : fork f g) : t.ι = t.π.app zero := rfl
+@[simp] lemma cofork.π_eq_app_one (t : cofork f g) : t.π = t.ι.app one := rfl
+
 @[simp, reassoc] lemma fork.app_zero_left (s : fork f g) :
   s.π.app zero ≫ f = s.π.app one :=
 by rw [←s.w left, parallel_pair_map_left]
@@ -175,38 +188,19 @@ def fork.of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : fork f g :=
 def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :=
 { X := P,
   ι :=
-  { app := λ X, begin cases X, exact f ≫ π, exact π, end,
-    naturality' := λ X Y f,
-    begin
-      cases X; cases Y; cases f; dsimp; simp,
-      { dsimp, simp, },
-      { exact w.symm },
-      { dsimp, simp, },
-    end } }
-
-/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms `t.π.app zero : t.X ⟶ X`
-    and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is interesting, and we give it the
-    shorter name `fork.ι t`. -/
-abbreviation fork.ι (t : fork f g) := t.π.app zero
-
-/-- A cofork `t` on the parallel_pair `f g : X ⟶ Y` consists of two morphisms
-    `t.ι.app zero : X ⟶ t.X` and `t.ι.app one : Y ⟶ t.X`. Of these, only the second one is
-    interesting, and we give it the shorter name `cofork.π t`. -/
-abbreviation cofork.π (t : cofork f g) := t.ι.app one
+  { app := λ X, walking_parallel_pair.cases_on X (f ≫ π) π,
+    naturality' := λ i j f, by { cases f; dsimp; simp [w] } } } -- See note [dsimp, simp]
 
-@[simp] lemma fork.ι_of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
-  fork.ι (fork.of_ι ι w) = ι := rfl
-@[simp] lemma cofork.π_of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
-  cofork.π (cofork.of_π π w) = π := rfl
-
-lemma fork.ι_eq_app_zero (t : fork f g) : fork.ι t = t.π.app zero := rfl
-lemma cofork.π_eq_app_one (t : cofork f g) : cofork.π t = t.ι.app one := rfl
+lemma fork.ι_of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
+  (fork.of_ι ι w).ι = ι := rfl
+lemma cofork.π_of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
+  (cofork.of_π π w).π = π := rfl
 
 @[reassoc]
-lemma fork.condition (t : fork f g) : fork.ι t ≫ f = fork.ι t ≫ g :=
+lemma fork.condition (t : fork f g) : t.ι ≫ f = t.ι ≫ g :=
 by rw [t.app_zero_left, t.app_zero_right]
 @[reassoc]
-lemma cofork.condition (t : cofork f g) : f ≫ cofork.π t = g ≫ cofork.π t :=
+lemma cofork.condition (t : cofork f g) : f ≫ t.π = g ≫ t.π :=
 by rw [t.left_app_one, t.right_app_one]
 
 /-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the
@@ -735,26 +729,18 @@ variables {C} [split_mono f]
 A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
 Here we build the cone, and show in `split_mono_equalizes` that it is a limit cone.
 -/
+@[simps {rhs_md := semireducible}]
 def cone_of_split_mono : cone (parallel_pair (𝟙 Y) (retraction f ≫ f)) :=
-fork.of_ι f (by tidy)
-
-@[simp] lemma cone_of_split_mono_π_app_zero : (cone_of_split_mono f).π.app zero = f := rfl
-@[simp] lemma cone_of_split_mono_π_app_one : (cone_of_split_mono f).π.app one = f ≫ 𝟙 Y := rfl
+fork.of_ι f (by simp)
 
 /--
 A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
 -/
 def split_mono_equalizes {X Y : C} (f : X ⟶ Y) [split_mono f] : is_limit (cone_of_split_mono f) :=
-{ lift := λ s, s.π.app zero ≫ retraction f,
-  fac' := λ s,
-  begin
-    rintros (⟨⟩|⟨⟩),
-    { rw [cone_of_split_mono_π_app_zero],
-      erw [category.assoc, ← s.π.naturality right, s.π.naturality left, category.comp_id], },
-    { erw [cone_of_split_mono_π_app_one, category.comp_id, category.assoc,
-            ← s.π.naturality right, category.id_comp], }
-  end,
-  uniq' := λ s m w, begin rw ←(w zero), simp, end, }
+fork.is_limit.mk' _ $ λ s,
+⟨s.ι ≫ retraction f,
+ by { dsimp, rw [category.assoc, ←s.condition], apply category.comp_id },
+ λ m hm, by simp [←hm]⟩
 
 end
 
@@ -766,26 +752,19 @@ variables {C} [split_epi f]
 A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
 Here we build the cocone, and show in `split_epi_coequalizes` that it is a colimit cocone.
 -/
+@[simps {rhs_md := semireducible}]
 def cocone_of_split_epi : cocone (parallel_pair (𝟙 X) (f ≫ section_ f)) :=
-cofork.of_π f (by tidy)
-
-@[simp] lemma cocone_of_split_epi_ι_app_one : (cocone_of_split_epi f).ι.app one = f := rfl
-@[simp] lemma cocone_of_split_epi_ι_app_zero : (cocone_of_split_epi f).ι.app zero = 𝟙 X ≫ f := rfl
+cofork.of_π f (by simp)
 
 /--
 A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
 -/
-def split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [split_epi f] : is_colimit (cocone_of_split_epi f) :=
-{ desc := λ s, section_ f ≫ s.ι.app one,
-  fac' := λ s,
-  begin
-    rintros (⟨⟩|⟨⟩),
-    { erw [cocone_of_split_epi_ι_app_zero, category.assoc, category.id_comp, ←category.assoc,
-            s.ι.naturality right, functor.const.obj_map, category.comp_id], },
-    { erw [cocone_of_split_epi_ι_app_one, ←category.assoc, s.ι.naturality right,
-            ←s.ι.naturality left, category.id_comp] }
-  end,
-  uniq' := λ s m w, begin rw ←(w one), simp, end, }
+def split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [split_epi f] :
+  is_colimit (cocone_of_split_epi f) :=
+cofork.is_colimit.mk' _ $ λ s,
+⟨section_ f ≫ s.π,
+ by { dsimp, rw [← category.assoc, ← s.condition, category.id_comp] },
+ λ m hm, by simp [← hm]⟩
 
 end