awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (hypothesis)
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.GuitartExact
have this₁ : 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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.GuitartExact
have mp : ((w ≫ᵥ w'.hom).vComp' w''.hom α β).GuitartExact
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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₁₂
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact
have rw : (w.vComp' w'.hom eL eR).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
Tactic: rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact
have rw₁ : ((w ≫ᵥ w'.hom).whiskerVertical eL.hom eR.inv).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
Tactic: rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact
have rw₂ : (w ≫ᵥ w'.hom).GuitartExact ↔ (w ≫ᵥ w'.hom).GuitartExact
Tactic: rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
have rw : α.hom ≫ α.inv ≫ (f ≫ β.hom) ≫ β.inv = f
Tactic: rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
have rw₁ : α.hom ≫ α.inv ≫ f ≫ β.hom ≫ β.inv = f
Tactic: rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
have rw₂ : α.hom ≫ α.inv ≫ f ≫ 𝟙 Y = f
Tactic: rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
have rw₃ : f ≫ 𝟙 Y = f
Tactic: rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
have rw₄ : f = f
Tactic: rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
have rw : α.inv ≫ α.hom ≫ (f ≫ β.inv) ≫ β.hom = f
Tactic: rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
have rw₁ : α.inv ≫ α.hom ≫ f ≫ β.inv ≫ β.hom = f
Tactic: rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
have rw₂ : α.inv ≫ α.hom ≫ f ≫ 𝟙 Y₁ = f
Tactic: rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
have rw₃ : f ≫ 𝟙 Y₁ = f
Tactic: rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.HomCongr (goal)
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
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
have rw₄ : f = f
Tactic: rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
have mp : IsIdempotentComplete.{v_1, u_1} C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
have mpr : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete.{v_1, u_1} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ HasEqualizer (𝟙 X) p
have mp : ∀ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p), HasEqualizer (𝟙 X) p
Tactic: rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ i ≫ 𝟙 X = i ≫ p
have rw : i = i ≫ p
Tactic: rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ i ≫ 𝟙 X = i ≫ p
have rw₁ : i = i ≫ e ≫ i
Tactic: rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ i ≫ 𝟙 X = i ≫ p
have rw₂ : i = (i ≫ e) ≫ i
Tactic: rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ i ≫ 𝟙 X = i ≫ p
have rw₃ : i = 𝟙 Y ≫ i
Tactic: rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ i ≫ 𝟙 X = i ≫ p
have rw₄ : i = i
Tactic: rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ IsLimit (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)
have create : (s : Fork (𝟙 X) p) →
  { l : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i sorry) //
    l ≫ Fork.ι (Fork.ofι i sorry) = s.ι ∧
      ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i sorry)}, m ≫ Fork.ι (Fork.ofι i sorry) = s.ι → m = l }
Tactic: apply Fork.IsLimit.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ { 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 }
have create : (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i sorry) = s.ι ∧
  ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i sorry)}, m ≫ Fork.ι (Fork.ofι i sorry) = s.ι → m = s.ι ≫ e
Tactic: refine ⟨s.ι ≫ e, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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.ι ∧
    ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i ⋯)}, m ≫ Fork.ι (Fork.ofι i ⋯) = s.ι → m = s.ι ≫ e
have create : (s.ι ≫ e) ≫ Fork.ι (Fork.ofι i sorry) = s.ι
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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.ι
⊢ (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
have create₁ : ∀ {m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 X) p) (Fork.ofι i sorry)}, m ≫ Fork.ι (Fork.ofι i sorry) = s.ι → m = s.ι ≫ e
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (hypothesis)
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 = s.ι ≫ e
have hm₁ : m ≫ i = s.ι
Tactic: rw [Fork.ι_ofι] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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 = s.ι ≫ e
have create : m = (m ≫ i) ≫ e
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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 ≫ i) ≫ e
have create : m = m ≫ 𝟙 Y
Tactic: simp only [assoc, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
have mpr : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (hypothesis)
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
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have this : HasEqualizer (𝟙 X) p
Tactic: haveI : HasEqualizer (𝟙 X) p := h X p hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ p ≫ 𝟙 X = p ≫ p
have rw : p ≫ 𝟙 X = p
Tactic: rw [hp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ p ≫ 𝟙 X = p ≫ p
have rw₁ : p = p
Tactic: rw [hp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have mpr : equalizer.ι (𝟙 X) p ≫ equalizer.lift p sorry = 𝟙 (equalizer (𝟙 X) p)
Tactic: refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)
have mpr : CategoryStruct.comp (Y := equalizer (𝟙 X) p) (equalizer.ι (𝟙 X) p ≫ equalizer.lift p sorry) (equalizer.ι (𝟙 X) p) =
  𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ CategoryStruct.comp (Y := equalizer (𝟙 X) p) (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) (equalizer.ι (𝟙 X) p) =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
have mpr : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ p) (equalizer.ι (𝟙 X) p)
Tactic: simp only [assoc, limit.lift_π, Fork.ofι_pt,
      Fork.ofι_π_app, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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
⊢ Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ p) (equalizer.ι (𝟙 X) p)
have mpr : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ 𝟙 X) (equalizer.ι (𝟙 X) p)
Tactic: rw [← equalizer.condition, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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)
⊢ Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p ≫ p) (equalizer.ι (𝟙 X) p)
have mpr₁ : Eq (α := equalizer (𝟙 X) p ⟶ X) (equalizer.ι (𝟙 X) p) (equalizer.ι (𝟙 X) p)
Tactic: rw [← equalizer.condition, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
have rw : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
Tactic: rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
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), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
have mp : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
mp : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
have mpr : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{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
⊢ HasKernel p
have this : HasEqualizer (𝟙 X) (𝟙 X - p)
Tactic: haveI : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{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) (𝟙 X - p)
⊢ HasKernel p
have h₁ : p = 𝟙 X - (𝟙 X - p)
Tactic: convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)