awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (inl : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) inl (desc (F.map f) (F.map g))
⊢ Eq (α := biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
    (desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
have h₁ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (inr : F.obj Y ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W) =
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) inr (desc (F.map f) (F.map g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W))
    (F.map (desc f g))
have rw : Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W)
  (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W))
  (F.map (desc f g))
Tactic: rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
rw :
  Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W))
    (F.map (desc f g))
⊢ Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W))
    (F.map (desc f g))
have rw₁ : Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W) (F.map (desc f g)) (F.map (desc f g))
Tactic: rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst_2 : HasEqualizer f g
inst_3 : PreservesLimit (parallelPair f g) G
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g) ≫ G.map f) (G.map (equalizer.ι f g) ≫ G.map g)
have simp : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst_2 : HasEqualizer f g
inst_3 : PreservesLimit (parallelPair f g) G
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))
have rw : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ g)) (G.map (equalizer.ι f g ≫ g))
Tactic: rw [equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
i : IsIso (X := G.obj (equalizer f g)) (Y := equalizer (G.map f) (G.map g)) (equalizerComparison f g G)
⊢ PreservesLimit (parallelPair f g) G
have apply : IsLimit (G.mapCone (Fork.ofι (P := equalizer f g) (equalizer.ι f g) sorry))
Tactic: apply preservesLimit_of_preserves_limit_cone (equalizerIsEqualizer f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
i : IsIso (X := G.obj (equalizer f g)) (Y := equalizer (G.map f) (G.map g)) (equalizerComparison f g G)
⊢ IsLimit (G.mapCone (Fork.ofι (P := equalizer f g) (equalizer.ι f g) ⋯))
have apply : IsLimit (Fork.ofι (P := G.obj (equalizer f g)) (G.map (equalizer.ι f g)) sorry)
Tactic: apply (isLimitMapConeForkEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
inst_4 : PreservesLimit (parallelPair f g) G
⊢ Eq (α := equalizer (G.map f) (G.map g) ⟶ G.obj X)
    (CategoryStruct.comp (Y := G.obj (equalizer f g)) (Iso.inv (iso G f g)) (G.map (equalizer.ι f g)))
    (equalizer.ι (G.map f) (G.map g))
have rw : 𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) =
  CategoryStruct.comp (Y := equalizer (G.map f) (G.map g)) (Iso.hom (iso G f g)) (equalizer.ι (G.map f) (G.map g))
Tactic: rw [← Iso.cancel_iso_hom_left (PreservesEqualizer.iso G f g), ← Category.assoc, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ Cofork.π
        ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))) ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
              (G.mapCocone (Cofork.ofπ h w))).pt) =
    (Cofork.ofπ (G.map h) ⋯).π
have dsimp : ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))).ι.app
      WalkingParallelPair.one ≫
    Iso.hom
      (Iso.refl
        ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
            (G.mapCocone (Cofork.ofπ h w))).pt) =
  G.map h
Tactic: dsimp only [Cofork.π, Cofork.ofπ_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))).ι.app
        WalkingParallelPair.one ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
              (G.mapCocone (Cofork.ofπ h w))).pt) =
    G.map h
have dsimp : (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
have rw : 𝟙 (G.obj Y) ≫ G.map h = G.map h
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
rw : 𝟙 (G.obj Y) ≫ G.map h = G.map h
⊢ (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
have rw₁ : G.map h = G.map h
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : HasCoequalizer f g
inst_3 : PreservesColimit (parallelPair f g) G
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map f ≫ G.map (coequalizer.π f g))
    (G.map g ≫ G.map (coequalizer.π f g))
have simp : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : HasCoequalizer f g
inst_3 : PreservesColimit (parallelPair f g) G
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
have rw : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (g ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
Tactic: rw [coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
i : IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
⊢ PreservesColimit (parallelPair f g) G
have apply : IsColimit (G.mapCocone (Cofork.ofπ (P := coequalizer f g) (coequalizer.π f g) sorry))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
i : IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (P := coequalizer f g) (coequalizer.π f g) ⋯))
have apply : IsColimit (Cofork.ofπ (P := G.obj (coequalizer f g)) (G.map (coequalizer.π f g)) sorry)
Tactic: apply (isColimitMapCoconeCoforkEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ G.map (coequalizer.π f g) ≫ h = G.map (coequalizer.π f g) ≫ k → h = k
have rw : CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
        (coequalizerComparison f g G) ≫
      h =
    CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
        (coequalizerComparison f g G) ≫
      k →
  h = k
Tactic: rw [← ι_comp_coequalizerComparison]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        h =
      CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        k →
    h = k
have this : Epi (Y := G.obj (coequalizer f g))
  (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (coequalizerComparison f g G))
Tactic: haveI : Epi (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) := by
      apply epi_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
⊢ Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.π (G.map f) (G.map g))
have rw : Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
  (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
      (Iso.inv (PreservesCoequalizer.iso G f g))))
  (coequalizer.π (G.map f) (G.map g))
Tactic: rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
rw :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
⊢ Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.π (G.map f) (G.map g))
have rw₁ : Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
  (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (Iso.hom (PreservesCoequalizer.iso G f g))
      (Iso.inv (PreservesCoequalizer.iso G f g))))
  (coequalizer.π (G.map f) (G.map g))
Tactic: rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
rw :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
rw₁ :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (Iso.hom (PreservesCoequalizer.iso G f g))
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
⊢ Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.π (G.map f) (G.map g))
have rw₂ : coequalizer.π (G.map f) (G.map g) ≫ 𝟙 (coequalizer (G.map f) (G.map g)) = coequalizer.π (G.map f) (G.map g)
Tactic: rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
rw :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
rw₁ :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (Iso.hom (PreservesCoequalizer.iso G f g))
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
rw₂ : coequalizer.π (G.map f) (G.map g) ≫ 𝟙 (coequalizer (G.map f) (G.map g)) = coequalizer.π (G.map f) (G.map g)
⊢ Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.π (G.map f) (G.map g))
have rw₃ : Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
  (coequalizer.π (G.map f) (G.map g))
Tactic: rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (coequalizer.desc k wk)) =
    k
have rw : CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.desc k wk) =
  k
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
rw :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
        (Iso.inv (PreservesCoequalizer.iso G f g)))
      (coequalizer.desc k wk) =
    k
⊢ CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (coequalizer.desc k wk)) =
    k
have rw₁ : CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g)) (coequalizer.desc k wk) =
  k
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
rw :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
        (Iso.inv (PreservesCoequalizer.iso G f g)))
      (coequalizer.desc k wk) =
    k
rw₁ :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizer.desc k wk) =
    k
⊢ CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (coequalizer.desc k wk)) =
    k
have rw₂ : k = k
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))))
    (q ≫ coequalizer.π f' g')
have rw : Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
  (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)))
  (q ≫ coequalizer.π f' g')
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]