awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((H₂ ⋙ eR.functor).map (eL.unit.app (L₁.obj X₁)) ≫
              (natTrans w'.hom).app ((eL.functor ⋙ eL.inverse).obj (L₁.obj X₁)) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
simp [← H₂.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
⊢ w = (w ≫ᵥ w'.hom).vComp' w''.hom α β

Tactic:
have : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β := by
      ext X₁
      simp? [w'', α, β] says
        simp only [Functor.comp_obj, vComp'_app, Iso.trans_inv, Functor.isoWhiskerLeft_inv,
          Iso.symm_inv, assoc, NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app,
          Functor.whiskerLeft_app, Functor.associator_inv_app, comp_id, id_comp, vComp_app,
          Functor.map_comp, Equivalence.inv_fun_map, CatCommSq.vInv_iso_hom_app, Iso.trans_hom,
          Functor.isoWhiskerLeft_hom, Iso.symm_hom, Functor.associator_hom_app,
          Functor.rightUnitor_hom_app, Iso.hom_inv_id_app_assoc, w'', α, β]
      simp only [hw', ← eR.inverse.map_comp_assoc]
      rw [Equivalence.counitInv_app_functor, ← Functor.comp_map, ← NatTrans.naturality_assoc]
      simp [← H₂.map_comp]
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this_2 : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
this : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β
mp : ((w ≫ᵥ w'.hom).vComp' w''.hom α β).GuitartExact
⊢ w.GuitartExact

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this_2 : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
this : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β
⊢ ((w ≫ᵥ w'.hom).vComp' w''.hom α β).GuitartExact

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
h : w.GuitartExact
⊢ (w ≫ᵥ w'.hom).GuitartExact

Tactic:
vComp w w'.hom

Premises used: CategoryTheory.Iso.hom, CategoryTheory.TwoSquare.GuitartExact.vComp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
h : w.GuitartExact
⊢ (w ≫ᵥ w'.hom).GuitartExact

Tactic:
exact vComp w w'.hom

Premises used: CategoryTheory.Iso.hom, CategoryTheory.TwoSquare.GuitartExact.vComp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
E : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
E' : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ E.functor ≅ L₁₂
eR : R₁ ⋙ E'.functor ≅ R₁₂
rw : (w.vComp' w'.hom eL eR).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
rw₁ : ((w ≫ᵥ w'.hom).whiskerVertical eL.hom eR.inv).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
rw₂ rw₃ : (w ≫ᵥ w'.hom).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]

Premises used: CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences, CategoryTheory.TwoSquare.vComp', CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
rw : α.hom ≫ α.inv ≫ (f ≫ β.hom) ≫ β.inv = f
rw₁ : α.hom ≫ α.inv ≫ f ≫ β.hom ≫ β.inv = f
rw₂ : α.hom ≫ α.inv ≫ f ≫ 𝟙 Y = f
rw₃ : f ≫ 𝟙 Y = f
rw₄ rw₅ : f = f
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f

Tactic:
rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
rw : α.inv ≫ α.hom ≫ (f ≫ β.inv) ≫ β.hom = f
rw₁ : α.inv ≫ α.hom ≫ f ≫ β.inv ≫ β.hom = f
rw₂ : α.inv ≫ α.hom ≫ f ≫ 𝟙 Y₁ = f
rw₃ : f ≫ 𝟙 Y₁ = f
rw₄ rw₅ : f = f
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f

Tactic:
rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := X₁ ⟶ Z₁) ((α.homCongr γ : (a : X ⟶ Z) → X₁ ⟶ Z₁) (f ≫ g) : X₁ ⟶ Z₁)
    (CategoryStruct.comp (Y := Y₁) ((α.homCongr β : (a : X ⟶ Y) → X₁ ⟶ Y₁) f)
        ((β.homCongr γ : (a : Y ⟶ Z) → Y₁ ⟶ Z₁) g) :
      X₁ ⟶ Z₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (homCongr (refl X) (refl Y) : (a : X ⟶ Y) → X ⟶ Y) f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ Eq (α := X₃ ⟶ Y₃) (((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂) : (a : X₁ ⟶ Y₁) → X₃ ⟶ Y₃) f : X₃ ⟶ Y₃)
    (((α₁.homCongr β₁).trans (α₂.homCongr β₂) : (a : X₁ ⟶ Y₁) → X₃ ⟶ Y₃) f : X₃ ⟶ Y₃)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
α : X₁ ≅ X₂
β : Y₁ ≅ Y₂
⊢ (α.homCongr β).symm = α.symm.homCongr β.symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.homCongr, rfl
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.LeftInverse (fun (h : X₂ ≅ Y₂) ↦ f ≪≫ h ≪≫ g.symm) fun (h : X₁ ≅ Y₁) ↦ f.symm ≪≫ h ≪≫ g

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.RightInverse (fun (h : X₂ ≅ Y₂) ↦ f ≪≫ h ≪≫ g.symm) fun (h : X₁ ≅ Y₁) ↦ f.symm ≪≫ h ≪≫ g

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ Eq (α := F.obj X₁ ⟶ F.obj Y₁) (F.map ((α.homCongr β : (a : X ⟶ Y) → X₁ ⟶ Y₁) f))
    (((F.mapIso α).homCongr (F.mapIso β) : (a : F.obj X ⟶ F.obj Y) → F.obj X₁ ⟶ F.obj Y₁) (F.map f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.HomCongr
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ Eq (α := F.obj X₁ ≅ F.obj Y₁) (F.mapIso ((α.isoCongr β : (a : X ≅ Y) → X₁ ≅ Y₁) f))
    (((F.mapIso α).isoCongr (F.mapIso β) : (a : F.obj X ≅ F.obj Y) → F.obj X₁ ≅ F.obj Y₁) (F.mapIso f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsIdempotentComplete.{v_1, u_1} C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
mpr : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
mp : ∀ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p), HasEqualizer (𝟙 X) p
⊢ HasEqualizer (𝟙 X) p

Tactic:
rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Premises used: CategoryTheory.IsIdempotentComplete.idempotents_split
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
rw : i = i ≫ p
rw₁ : i = i ≫ e ≫ i
rw₂ : i = (i ≫ e) ≫ i
rw₃ : i = 𝟙 Y ≫ i
rw₄ rw₅ : i = i
⊢ i ≫ 𝟙 X = i ≫ p

Tactic:
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
create :
  (s : Fork (𝟙 X) p) →
    { l : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯) //
      l ≫ Fork.ι (Fork.ofι i ⋯) = s.ι ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = l }
⊢ IsLimit (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)

Tactic:
apply Fork.IsLimit.mk'

Premises used: CategoryTheory.Limits.Fork.IsLimit.mk'
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
create :
  (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i ⋯) = s.ι ∧
    ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = s.ι ≫ e
⊢ { l : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯) //
    l ≫ Fork.ι (Fork.ofι i ⋯) = s.ι ∧
      ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = l }

Tactic:
refine ⟨s.ι ≫ e, ?_⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
create : (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i ⋯) = s.ι
create₁ :
  ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = s.ι ≫ e
⊢ (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i ⋯) = s.ι ∧
    ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = s.ι ≫ e

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i ⋯) = s.ι

Tactic:
simp [h₂, ← Limits.Fork.condition s]

Premises used: CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
hm : m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι
⊢ m ≫ i = s.ι

Tactic:
rw [Fork.ι_ofι] at hm

Premises used: CategoryTheory.Limits.Fork.ι_ofι
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
hm : m ≫ i = s.ι
create : m = (m ≫ i) ≫ e
⊢ m = s.ι ≫ e

Tactic:
rw [← hm]
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
hm : m ≫ i = s.ι
create : m = m ≫ 𝟙 Y
⊢ m = (m ≫ i) ≫ e

Tactic:
simp only [assoc, h₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
hm : m ≫ i = s.ι
⊢ m = m ≫ 𝟙 Y

Tactic:
(comp_id m).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
hm : m ≫ i = s.ι
⊢ m = m ≫ 𝟙 Y

Tactic:
exact (comp_id m).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ HasEqualizer (𝟙 X) p

Tactic:
exact
      ⟨Nonempty.intro
          { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
            isLimit := by
              apply Fork.IsLimit.mk'
              intro s
              refine ⟨s.ι ≫ e, ?_⟩
              constructor
              · simp [h₂, ← Limits.Fork.condition s]
              · intro m hm
                rw [Fork.ι_ofι] at hm
                rw [← hm]
                simp only [assoc, h₁]
                exact (comp_id m).symm }⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete.{v_1, u_1} C

Tactic:
⟨?_⟩

Premises used: CategoryTheory.IsIdempotentComplete.mk
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
mpr : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ IsIdempotentComplete.{v_1, u_1} C

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p

Tactic:
haveI : HasEqualizer (𝟙 X) p := h X p hp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
rw : p ≫ 𝟙 X = p
rw₁ rw₂ : p = p
⊢ p ≫ 𝟙 X = p ≫ p

Tactic:
rw [hp, comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
mpr : equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
mpr :
  CategoryStruct.comp (Y := equalizer (𝟙 X) p) (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) (equalizer.ι (𝟙 X) p) =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
mpr : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ p) (equalizer.ι (𝟙 X) p)
⊢ CategoryStruct.comp (Y := equalizer (𝟙 X) p) (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) (equalizer.ι (𝟙 X) p) =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p

Tactic:
simp only [assoc, limit.lift_π, Fork.ofι_pt,
      Fork.ofι_π_app, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.ofι_pt, CategoryTheory.Limits.Fork.ofι_π_app, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
mpr : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ 𝟙 X) (equalizer.ι (𝟙 X) p)
mpr₁ mpr₂ : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p) (equalizer.ι (𝟙 X) p)
⊢ Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ p) (equalizer.ι (𝟙 X) p)

Tactic:
rw [← equalizer.condition, comp_id]

Premises used: CategoryTheory.Limits.equalizer.condition, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ (𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p

Tactic:
simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]

Premises used: sub_self, sub_zero, CategoryTheory.Category.comp_id, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp