awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₇ : (π ≫ x₄) ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
rw₇ : (π ≫ x₄) ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₈ : π ≫ x₄ ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
rw₇ : (π ≫ x₄) ≫ k = 0
rw₈ : π ≫ x₄ ≫ k = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₉ : Eq (α := T₁ ⟶ X₅) (π ≫ 0) 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
rw₇ : (π ≫ x₄) ≫ k = 0
rw₈ : π ≫ x₄ ≫ k = 0
rw₉ : Eq (α := T₁ ⟶ X₅) (π ≫ 0) 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₁₀ : Eq.{v + 1} (α := T₁ ⟶ X₅) 0 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₄ = 0
have fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
Tactic: have fac₃ : (-x₂) ≫ r' = x₃ ≫ b' := by
      rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ ∃ (x₂' : T₁ ⟶ X₂), π ≫ x₄ = x₂' ≫ r
have refine : π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
Tactic: refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw₂ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₂ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw₃ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ l ≫ b
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₂ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
rw₃ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ l ≫ b
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw₄ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + x₃ ≫ b
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₂ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
rw₃ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ l ≫ b
rw₄ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + x₃ ≫ b
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
have rw₅ : x₃ ≫ b + x₂ ≫ r = x₃ ≫ b + x₂ ≫ r
Tactic: rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₄ = 0
have obtain : ∀ (x₂' : T₁ ⟶ X₂) (hx₂' : π ≫ x₄ = x₂' ≫ r), x₄ = 0
Tactic: obtain ⟨x₂', hx₂'⟩ : ∃ x₂', π ≫ x₄ = x₂' ≫ r := by
      refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩
      rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0
have rw : Epi π →
  ∀ (x₂ : T₁ ⟶ X₂) (x₃ : T₁ ⟶ X₃) (eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b) (fac₃ : (-x₂) ≫ r' = x₃ ≫ b') (x₂' : T₁ ⟶ X₂)
    (hx₄ : x₂' ≫ r' = 0) (hx₂' : π ≫ x₄ = x₂' ≫ r), x₄ = 0
Tactic: rw [← cancel_epi π, comp_zero, reassoc_of% hx₂', fac₁] at hx₄
Cleared hypotheses: hx₄, w, x₂, x₃, eq, fac₃, x₂', hx₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0
have hx₅ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
Tactic: obtain rfl := zero_of_comp_mono _ hx₄
Cleared hypotheses: x₂', hx₄, hx₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
hx₅ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
⊢ x₄ = 0
have hx₂'₁ : π ≫ x₄ = 0 ≫ r
Tactic: obtain rfl := zero_of_comp_mono _ hx₄
Cleared hypotheses: x₂', hx₄, hx₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0 ≫ r
⊢ x₄ = 0
have hx₂'₁ : π ≫ x₄ = 0
Tactic: rw [zero_comp] at hx₂'
Cleared hypotheses: hx₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0
have rw : π ≫ x₄ = π ≫ 0
Tactic: rw [← cancel_epi π, hx₂', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0
rw : π ≫ x₄ = π ≫ 0
⊢ x₄ = 0
have rw₁ : Eq (α := T₁ ⟶ X₄) 0 (π ≫ 0)
Tactic: rw [← cancel_epi π, hx₂', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0
rw : π ≫ x₄ = π ≫ 0
rw₁ : Eq (α := T₁ ⟶ X₄) 0 (π ≫ 0)
⊢ x₄ = 0
have rw₂ : Eq.{v + 1} (α := T₁ ⟶ X₄) 0 0
Tactic: rw [← cancel_epi π, hx₂', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
⊢ Mono (X := cokernel t) (Y := cokernel b) (cokernel.map t b l r ⋯)
have rw : ∀ (P : C) (g : P ⟶ cokernel t), Eq (α := P ⟶ cokernel b) (g ≫ cokernel.map t b l r sorry) 0 → g = 0
Tactic: rw [Preadditive.mono_iff_cancel_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
⊢ z = 0
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀), Epi π₁ → ∀ (x₂ : A₁ ⟶ X₂) (hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t), z = 0
Tactic: obtain ⟨A₁, π₁, _, x₂, hx₂⟩ :=
    surjective_up_to_refinements_of_epi (cokernel.π t) z
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
⊢ z = 0
have this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) sorry)
Tactic: have : (ShortComplex.mk _ _ (cokernel.condition b)).Exact :=
    ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel b)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
⊢ z = 0
have obtain : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
  Epi π₂ →
    ∀ (x₃ : A₂ ⟶ ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) sorry))
      (hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) sorry)), z = 0
Tactic: obtain ⟨A₂, π₂, _, x₃, hx₃⟩ := this.exact_up_to_refinements (x₂ ≫ r) (by
    simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₃ : A₂ ⟶ ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
⊢ z = 0
have obtain : ∀ (x₁ : A₂ ⟶ X₁) (hx₁ : x₁ ≫ t = π₂ ≫ x₂)
  (hx₃ : π₂ ≫ x₂ ≫ r = (x₁ ≫ l) ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) sorry)), z = 0
Tactic: obtain ⟨x₁, hx₁, rfl⟩ := sq.exists_lift (π₂ ≫ x₂) x₃ (by simpa)
Cleared hypotheses: x₃, hx₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
⊢ Epi (X := kernel t) (Y := kernel b) (kernel.map t b l r ⋯)
have rw : ∀ ⦃A : C⦄ (y : A ⟶ kernel b), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ y = x ≫ kernel.map t b l r sorry
Tactic: rw [epi_iff_surjective_up_to_refinements]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r ⋯
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀),
  Epi π₁ →
    ∀
      (x₁ :
        A₁ ⟶
          ShortComplex.X₁
            (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
              Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) sorry.cokernelCofork)
              (biprod.lift t (-l)) (Cofork.π sorry.cokernelCofork) sorry))
      (hx₁ :
        π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
          x₁ ≫
            ShortComplex.f
              (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
                Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) sorry.cokernelCofork)
                (biprod.lift t (-l)) (Cofork.π sorry.cokernelCofork) sorry)),
      ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r sorry
Tactic: obtain ⟨A₁, π₁, _, x₁, hx₁⟩ := ((ShortComplex.mk _ _
    sq.cokernelCofork.condition).exact_of_g_is_cokernel
      sq.isColimitCokernelCofork).exact_up_to_refinements
        (z ≫ kernel.ι _ ≫ biprod.inr) (by simp)