awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
w :
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j :
        F.obj (f j) ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j) (desc fun (j : J) ↦ F.map (g j))
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (ι (F.obj ∘ f) j : (F.obj ∘ f) j ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (ι (F.obj ∘ f) j) (desc fun (j : J) ↦ F.map (g j))

Tactic:
dsimp only [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j :
        F.obj (f j) ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j) (desc fun (j : J) ↦ F.map (g j))

Tactic:
simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapBiproduct_inv, CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
rw :
  Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
    (F.map (desc g))
rw₁ rw₂ : Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W) (F.map (desc g)) (F.map (desc g))
⊢ Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (desc fun (j : J) ↦ F.map (g j) : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
    (F.map (desc g))

Tactic:
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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 : W ⟶ X
g : W ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (fst : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj X) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (snd : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj Y) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) snd
⊢ Eq (α := F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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 : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (fst : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj X) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) fst

Tactic:
simp [mapBiprod, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapBiprod
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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 : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (snd : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj Y) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) snd

Tactic:
simp [mapBiprod, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapBiprod
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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 : W ⟶ X
g : W ⟶ Y
rw :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
rw₁ :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g))
      (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))
        (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))))
    (F.map (lift f g))
rw₂ : F.map (lift f g) ≫ 𝟙 (F.obj (biprod.{v₁, u₁} X Y)) = F.map (lift f g)
rw₃ rw₄ : Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (F.map (lift f g))
⊢ Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))

Tactic:
rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.map_lift_mapBiprod
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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))
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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
⊢ 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))

Tactic:
simp [mapBiprod, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapBiprod
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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
⊢ 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:
simp [mapBiprod, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapBiprod
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
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))
rw₁ rw₂ : Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj W) (F.map (desc f g)) (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))

Tactic:
rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
⊢ Iso.hom
        (Iso.refl
          ((Cone.postcompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).hom).obj (G.mapCone (Fork.ofι h w))).pt) ≫
      (Fork.ofι (G.map h) ⋯).ι =
    Fork.ι ((Cone.postcompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).hom).obj (G.mapCone (Fork.ofι h w)))

Tactic:
simp [Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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 : ReflectsLimit (parallelPair f g) G
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
simp : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι 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)

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
rw rw₁ : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ g)) (G.map (equalizer.ι f g ≫ g))
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))

Tactic:
rw [equalizer.condition]

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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)
apply : IsLimit (G.mapCone (Fork.ofι (P := equalizer f g) (equalizer.ι f g) ⋯))
⊢ PreservesLimit (parallelPair f g) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (equalizerIsEqualizer f g)

Premises used: CategoryTheory.Limits.equalizerIsEqualizer, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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)
apply : IsLimit (Fork.ofι (P := G.obj (equalizer f g)) (G.map (equalizer.ι f g)) ⋯)
⊢ IsLimit (G.mapCone (Fork.ofι (P := equalizer f g) (equalizer.ι f g) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConeForkEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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 (Fork.ofι (P := G.obj (equalizer f g)) (G.map (equalizer.ι f g)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (parallelPair (G.map f) (G.map g))) i

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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 (α := G.obj (equalizer f g) ⟶ equalizer (G.map f) (G.map g)) (Iso.hom (iso G f g)) (equalizerComparison f g G)

Tactic:
rfl

Premises used: CategoryTheory.Limits.equalizerComparison, CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
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))
⊢ 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))

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesEqualizer.iso G f g), ← Category.assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.Limits.PreservesEqualizer.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
⊢ 𝟙 (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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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 : HasEqualizer (G.map f) (G.map g)
inst_4 : PreservesLimit (parallelPair f g) G
⊢ IsIso (X := G.obj (equalizer f g)) (Y := equalizer (G.map f) (G.map g)) (Iso.hom (PreservesEqualizer.iso G f g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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.map f ≫ G.map h = G.map g ≫ G.map h

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
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
⊢ 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) ⋯).π

Tactic:
dsimp only [Cofork.π, Cofork.ofπ_ι_app]

Premises used: CategoryTheory.Limits.Cofork.ofπ_ι_app, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
dsimp : (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
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
rw₁ rw₂ : G.map h = G.map h
⊢ (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp