awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0
have refine_1 : biprod.inl ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inl 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
refine_1 :
  biprod.inl ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inl 0
⊢ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0
have refine_1₁ : biprod.inr ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inr 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
      HAdd.hAdd (α :=
        { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
          biprod.{v_1, u_1} { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
            { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
        (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) =
    𝟙
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁
have h₀ : (biprod.inl ≫
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := sorry : ShortComplex.{v_1, u_1} C }.f ≫
        HAdd.hAdd (α :=
          { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
            biprod.{v_1, u_1}
              { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
              { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
          (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
    biprod.fst =
  (biprod.inl ≫
      𝟙
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := sorry : ShortComplex.{v_1, u_1} C }.X₁) ≫
    biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ HAdd.hAdd (α :=
          { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
            biprod.{v_1, u_1}
              { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
              { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
          (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := ⋯ : ShortComplex.{v_1, u_1} C }.f +
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := ⋯ : ShortComplex.{v_1, u_1} C }.g ≫
        σ₂.s ≫ σ₁.s =
    𝟙
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
have dsimp : HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
      HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
    (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
  𝟙 X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
      (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
have h : g₁ ≫
    (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.f +
        { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.g ≫ σ₂.s) ≫
      σ₁.s =
  g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₂ ≫ σ₁.s
Tactic: have h := g₁ ≫= σ₂.id =≫ σ₁.s
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
h :
  g₁ ≫
      (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.f +
          { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.g ≫ σ₂.s) ≫
        σ₁.s =
    g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₂ ≫ σ₁.s
⊢ HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
      (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
have h₁ : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
Tactic: simp only [add_comp, assoc, comp_add, id_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
h : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
      (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
have rw : HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
      HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
    (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
  σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.f +
    (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
Tactic: rw [← σ₁.id, ← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
h : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
      (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.f +
      (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
have simp : σ₁.r ≫ f₁ + g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = σ₁.r ≫ f₁ + (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
Tactic: simp only [comp_add, add_comp, assoc, BinaryBicone.inl_fst_assoc,
              BinaryBicone.inr_fst_assoc, zero_comp, comp_zero, add_zero,
              BinaryBicone.inl_snd_assoc, BinaryBicone.inr_snd_assoc, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
⊢ epiWithInjectiveKernel f'
have this : Epi f'
Tactic: have : Epi f' :=
      (MorphismProperty.epimorphisms C).of_retract r (.infer_property _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
this : Epi f'
⊢ CategoryStruct.comp (Y := kernel f) (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯)
      (kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯) =
    𝟙 (kernel f')
have h : CategoryStruct.comp (Y := equalizer f' 0)
    (CategoryStruct.comp (Y := kernel f) (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) sorry)
      (kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) sorry))
    (equalizer.ι f' 0) =
  𝟙 (kernel f') ≫ equalizer.ι f' 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
hp : epiWithInjectiveKernel p
A B : C
i : A ⟶ B
inst_2 : Mono i
⊢ HasLiftingProperty i p
have suffices : MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
Tactic: suffices (MorphismProperty.monomorphisms C).rlp p from this _ inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
hp : epiWithInjectiveKernel p
A B : C
i : A ⟶ B
inst_2 : Mono i
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
have rw : ∀
  (hp :
    ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ p = 0),
      Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := p, zero := w : ShortComplex.{v_1, u_1} C }.Splitting)
  {A B : C} (i : A ⟶ B) [Mono i], MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
Tactic: rw [epiWithInjectiveKernel_iff] at hp
Cleared hypotheses: hp, A, B, i, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
hp :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ p = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := p, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
A B : C
i : A ⟶ B
inst_2 : Mono i
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
have obtain : ∀ (I : C),
  Injective.{v_1, u_1} I →
    ∀ (s : I ⟶ X) (hs : s ≫ p = 0)
      (σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting),
      MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
Tactic: obtain ⟨I, _, s, hs, ⟨σ⟩⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
have hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
Tactic: have hI : (MorphismProperty.monomorphisms C).rlp (0 : I ⟶ 0) :=
    fun _ _ _ _ ↦ Injective.hasLiftingProperty_of_isZero _ _ (isZero_zero C)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
have refine : IsLimit (F :=
  cospan (X := { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
    0) 0 0)
  (PullbackCone.mk σ.r p sorry)
Tactic: refine MorphismProperty.of_isPullback (f' := σ.r) (f := 0) ⟨by simp, ⟨?_⟩⟩ hI
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
⊢ IsLimit (F :=
    cospan (X := { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y)
      (Z := 0) 0 0)
    (PullbackCone.mk σ.r p ⋯)
have refine : ∀
  (t :
    PullbackCone.{v_1, u_1} (C := C) (X :=
      { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z := 0) 0 0)
  (m : t.pt ⟶ { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₂)
  (hm₁ : m ≫ σ.r = t.fst) (hm₂ : m ≫ p = t.snd),
  m =
    (fun
          (t :
            PullbackCone.{v_1, u_1} (C := C) (X :=
              { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
              0) 0 0) ↦
        t.fst ≫ s + t.snd ≫ σ.s)
      t
Tactic: refine PullbackCone.IsLimit.mk _ (fun t ↦ t.fst ≫ s + t.snd ≫ σ.s)
    (fun t ↦ by simp [dsimp% σ.f_r]) (fun t ↦ by simp [hs, dsimp% σ.s_g]) (fun t m hm₁ hm₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
have rw : Epi (Y := kernel S.g) (kernel.lift S.g S.f sorry) ↔
  Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g)
Tactic: rw [S.exact_iff_epi_kernel_lift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) ↔
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
have this : Eq (α := S.X₁ ⟶ kernel S.g)
  (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
      (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) :
    S.X₁ ⟶ kernel S.g)
  (kernel.lift S.g S.f sorry : S.X₁ ⟶ kernel S.g)
Tactic: have : factorThruImage S.f ≫ imageToKernel' S.f S.g S.zero = kernel.lift S.g S.f S.zero := by
    simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
      Category.assoc, image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) ↔
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
have mp : Epi (Y := kernel S.g) (kernel.lift S.g S.f sorry) →
  Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
mp :
  Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) →
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) ↔
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
have mpr : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) →
  Epi (Y := kernel S.g) (kernel.lift S.g S.f sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
h : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
have mpr : Epi (Y := kernel S.g)
  (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
      (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) :
    S.X₁ ⟶ kernel S.g)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔
    Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
have rw : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) ↔
  Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: rw [S.exact_iff_epi_imageToKernel']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) ↔
    Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
have apply : Arrow.mk (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) ≅
  Arrow.mk (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔ IsIso (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
have simp : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g) →
  Mono (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g sorry : image S.f ⟶ kernel S.g)
Tactic: simp only [S.exact_iff_epi_imageToKernel', isIso_iff_mono_and_epi, iff_and_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔
    IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
have rw : Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry) ↔
  IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: rw [S.exact_iff_epi_imageToKernel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) ↔
    IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
have mp : Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry) →
  IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: constructor