awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have mp : Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have mpr : (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f) → Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
⊢ Epi f
have mpr : ∀ (A : C) (π : A ⟶ Y) (hπ : Epi π) (a' : A ⟶ X) (fac : π ≫ 𝟙 Y = a' ≫ f), Epi f
Tactic: obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π ≫ 𝟙 Y = a' ≫ f
⊢ Epi f
have fac₁ : π = a' ≫ f
Tactic: rw [comp_id] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ S.Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
have rw : (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) ↔
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
Tactic: rw [S.exact_iff_epi_toCycles, epi_iff_surjective_up_to_refinements]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
have mp : (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) →
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
mp :
  (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
have mpr : (∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f) →
  ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ a = x₁ ≫ S.f
have mp : ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.X₁)
  (fac : Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles a ha) (x₁ ≫ S.toCycles)),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ a = x₁ ≫ S.f
Tactic: obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ a = x ≫ S.toCycles
have mpr : ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.X₁) (fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ a = x ≫ S.toCycles
Tactic: obtain ⟨A', π, hπ, x₁, fac⟩ := hS (a ≫ S.iCycles) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
have rw : ∀
  (hS :
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f)
  {A : C} (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS
Cleared hypotheses: hS, A, x₂, hx₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
have obtain : ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (z : A' ⟶ S.cycles) (hz : π ≫ γ = z ≫ S.homologyπ),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
Tactic: obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
have refine : π ≫ γ = S.liftCycles (z ≫ S.iCycles) sorry ≫ S.homologyπ
Tactic: refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ π ≫ γ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ
have rw : Eq (α := A' ⟶ S.homology) (z ≫ S.homologyπ) (S.liftCycles (z ≫ S.iCycles) sorry ≫ S.homologyπ)
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ Eq (α := A' ⟶ S.homology) (z ≫ S.homologyπ) (S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ)
have e_a : z = S.liftCycles (z ≫ S.iCycles) sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ z = S.liftCycles (z ≫ S.iCycles) ⋯
have e_a : z ≫ S.iCycles = CategoryStruct.comp (Y := S.cycles) (S.liftCycles (z ≫ S.iCycles) sorry) S.iCycles
Tactic: rw [← cancel_mono S.iCycles, liftCycles_i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
e_a : z ≫ S.iCycles = CategoryStruct.comp (Y := S.cycles) (S.liftCycles (z ≫ S.iCycles) ⋯) S.iCycles
⊢ z = S.liftCycles (z ≫ S.iCycles) ⋯
have e_a₁ : z ≫ S.iCycles = z ≫ S.iCycles
Tactic: rw [← cancel_mono S.iCycles, liftCycles_i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have refine_1 : ∀ (hy : y ≫ Cofork.π c = 0), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
Tactic: refine ⟨fun hy ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
refine_1 : ∀ (hy : y ≫ Cofork.π c = 0), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
⊢ y ≫ Cofork.π c = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have refine_2 : (∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0
Tactic: refine ⟨fun hy ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have h : { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: have h := (ShortComplex.mk _ _ c.condition).exact_of_g_is_cokernel
      (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h : { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have h₁ : ∀ ⦃A : C⦄
  (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry : ShortComplex.{v_1, u_1} C }.X₂),
  x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry : ShortComplex.{v_1, u_1} C }.g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
      A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry : ShortComplex.{v_1, u_1} C }.X₁),
      π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry }.f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄
    (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
have refine_1 : ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π)
  (x₁ : A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry : ShortComplex.{v_1, u_1} C }.X₁)
  (fac : π ≫ y = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := sorry }.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
Tactic: obtain ⟨A', π, hπ, x₁, fac⟩ := h y hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
have this : Eq (α :=
    A ⟶
      Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
        (CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry : CokernelCofork (Y := S.cycles) S.toCycles))
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂ : A ⟶ S.cycles)
        (Cofork.π (CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry) :
          S.cycles ⟶
            Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
              (CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry : CokernelCofork (Y := S.cycles) S.toCycles)) :
      A ⟶
        Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
          (CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry : CokernelCofork (Y := S.cycles) S.toCycles))
    (0 :
      A ⟶
        Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
          (CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry : CokernelCofork (Y := S.cycles) S.toCycles)) ↔
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁),
    Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x ≫ S.toCycles)
Tactic: have := CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
        S.homologyIsCokernel (S.liftCycles x₂ hx₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f
have suffices : Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
  Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') sorry ≫ S.homologyπ) 0
Tactic: suffices S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
      S.liftCycles (x₂ - x₂') (by simp [hx₂, hx₂']) ≫ S.homologyπ = 0 by
    simp [this, S.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements,
      sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
have rw : HSub.hSub (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) = 0 ↔
  Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') sorry ≫ S.homologyπ) 0
Tactic: rw [← sub_eq_zero, ← sub_comp, sub_liftCycles]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
rw :
  HSub.hSub (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) = 0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
have rw₁ : Eq (α := A ⟶ S.homology) (HSub.hSub (α := A ⟶ S.cycles) (S.liftCycles x₂ hx₂) (S.liftCycles x₂' hx₂') ≫ S.homologyπ) 0 ↔
  Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') sorry ≫ S.homologyπ) 0
Tactic: rw [← sub_eq_zero, ← sub_comp, sub_liftCycles]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
rw :
  HSub.hSub (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) = 0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
rw₁ :
  Eq (α := A ⟶ S.homology) (HSub.hSub (α := A ⟶ S.cycles) (S.liftCycles x₂ hx₂) (S.liftCycles x₂' hx₂') ≫ S.homologyπ)
      0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
have rw₂ : Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') sorry ≫ S.homologyπ) 0 ↔
  Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') sorry ≫ S.homologyπ) 0
Tactic: rw [← sub_eq_zero, ← sub_comp, sub_liftCycles]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ : A ⟶ S.cycles
⊢ Eq (α := A ⟶ S.homology) (z₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ z₂ = x₁ ≫ S.toCycles
have obtain : ∀ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0),
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
      Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x₁ ≫ S.toCycles)
Tactic: obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles, liftCycles_i]⟩
Cleared hypotheses: z₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ z₂' : A ⟶ S.cycles
⊢ Eq (α := A ⟶ S.homology) (z₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ z₂ = π ≫ z₂' + x₁ ≫ S.toCycles
have obtain : ∀ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0),
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ S.liftCycles x₂ hx₂ = π ≫ z₂' + x₁ ≫ S.toCycles
Tactic: obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles]⟩
Cleared hypotheses: z₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ S.liftCycles x₂ hx₂ = π ≫ z₂' + x₁ ≫ S.toCycles
have obtain : ∀ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0),
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
      π ≫ S.liftCycles x₂ hx₂ = HAdd.hAdd (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂' hx₂') (x₁ ≫ S.toCycles)
Tactic: obtain ⟨x₂', hx₂', rfl⟩ : ∃ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0), z₂' =
    S.liftCycles x₂' hx₂' := ⟨z₂' ≫ S.iCycles, by simp,
      by simp [← cancel_mono S.iCycles]⟩
Cleared hypotheses: z₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
have refine_1 : ∀ (h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)) (A : C) (x₂ : A ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0)
  (y₁ : A ⟶ S₂.X₁) (fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
Tactic: refine ⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
refine_1 :
  ∀ (h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)) (A : C) (x₂ : A ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0)
    (y₁ : A ⟶ S₂.X₁) (fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
have refine_2 : ∀
  (h :
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f),
  Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
Tactic: refine ⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
have refine_1 : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
Tactic: suffices S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0 by
      rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
have refine_1 : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ x₂ ≫ φ.τ₂ = x₁ ≫ S₂.f
Tactic: simp only [← cancel_mono (homologyMap φ), zero_comp, assoc,
      homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      S₂.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Refinements (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have refine_2 : ∀ (P : C) (g : P ⟶ S₁.homology), Eq (α := P ⟶ S₂.homology) (g ≫ homologyMap φ) 0 → g = 0
Tactic: rw [Preadditive.mono_iff_cancel_zero]