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
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
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
⊢ γ = 0
have refine_2 : ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (z : A₁ ⟶ S₁.X₂) (hz : z ≫ S₁.g = 0)
  (fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ), γ = 0
Tactic: obtain ⟨A₁, π₁, hπ₁, z, hz, fac⟩ := S₁.eq_liftCycles_homologyπ_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
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ γ = 0
have refine_2 : Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
Tactic: rw [← cancel_epi π₁, fac, comp_zero]
-- 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₁ 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
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have hγ₁ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ γ ≫ homologyMap φ) (π₁ ≫ 0)
Tactic: replace hγ := π₁ ≫= hγ
Cleared hypotheses: hγ
-- 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₁ 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ γ ≫ homologyMap φ) (π₁ ≫ 0)
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have hγ₁ : ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁),
  Eq (α := A' ⟶ S₂.cycles) (π ≫ S₂.liftCycles (z ≫ φ.τ₂) sorry) (x₁ ≫ S₂.toCycles)
Tactic: simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_zero, comp_homologyπ_eq_zero_iff_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
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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
hγ :
  ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁),
    Eq (α := A' ⟶ S₂.cycles) (π ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (x₁ ≫ S₂.toCycles)
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have refine_2 : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (y : A₂ ⟶ S₂.X₁)
  (hy : Eq (α := A₂ ⟶ S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) sorry) (y ≫ S₂.toCycles)),
  Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
Tactic: obtain ⟨A₂, π₂, hπ₂, y, hy⟩ := hγ
Cleared hypotheses: hγ
-- 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₁ 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : Eq (α := A₂ ⟶ S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (y ≫ S₂.toCycles)
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have hy₁ : CategoryStruct.comp (Y := S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) sorry) S₂.iCycles =
  CategoryStruct.comp (Y := S₂.cycles) (y ≫ S₂.toCycles) S₂.iCycles
Tactic: replace hy := hy =≫ S₂.iCycles
Cleared hypotheses: 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₁ 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy :
  CategoryStruct.comp (Y := S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) S₂.iCycles =
    CategoryStruct.comp (Y := S₂.cycles) (y ≫ S₂.toCycles) S₂.iCycles
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have hy₁ : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
Tactic: simp only [assoc, liftCycles_i, toCycles_i] at hy
Cleared hypotheses: 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
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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ S₁.g = 0
have rw : π₂ ≫ z ≫ S₁.g = 0
Tactic: rw [assoc, hz, comp_zero]
-- 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
rw : π₂ ≫ z ≫ S₁.g = 0
⊢ (π₂ ≫ z) ≫ S₁.g = 0
have rw₁ : Eq (α := A₂ ⟶ S₁.X₃) (π₂ ≫ 0) 0
Tactic: rw [assoc, hz, comp_zero]
-- 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
rw : π₂ ≫ z ≫ S₁.g = 0
rw₁ : Eq (α := A₂ ⟶ S₁.X₃) (π₂ ≫ 0) 0
⊢ (π₂ ≫ z) ≫ S₁.g = 0
have rw₂ : Eq.{v_1 + 1} (α := A₂ ⟶ S₁.X₃) 0 0
Tactic: rw [assoc, hz, comp_zero]
-- 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have refine_2 : ∀ (A₃ : C) (π₃ : A₃ ⟶ A₂) (hπ₃ : Epi π₃) (x₁ : A₃ ⟶ S₁.X₁) (hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f),
  Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
Tactic: obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ :=
      h (π₂ ≫ z) (by rw [assoc, hz, comp_zero]) y (by simpa)
-- 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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
have refine_2 : ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ z = x₁ ≫ S₁.f
Tactic: rw [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₂
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have rw : (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) ↔
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Tactic: rw [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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have mp : (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) →
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
mp :
  (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have mpr : (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have mp : ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (γ : A₁ ⟶ S₁.homology)
  (hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Tactic: obtain ⟨A₁, π₁, hπ₁, γ, hγ⟩ := h (S₂.liftCycles y₂ hy₂ ≫ 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have mp : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (x₂ : A₂ ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0)
  (fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Tactic: obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have hγ₁ : Eq (α := A₂ ⟶ S₂.homology) (π₂ ≫ π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (π₂ ≫ γ ≫ homologyMap φ)
Tactic: replace hγ := π₂ ≫= hγ
Cleared hypotheses: hγ
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
hγ : Eq (α := A₂ ⟶ S₂.homology) (π₂ ≫ π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (π₂ ≫ γ ≫ homologyMap φ)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have hγ₁ : ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ π₁ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
Tactic: simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_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
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
hγ : ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ π₁ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
have mp : ∀ (A₃ : C) (π₃ : A₃ ⟶ A₂) (hπ₃ : Epi π₃) (x₁ : A₃ ⟶ S₂.X₁) (hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Tactic: obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := 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
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
have mpr : ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (y₂ : A₁ ⟶ S₂.X₂) (hy₂ : y₂ ≫ S₂.g = 0)
  (fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
Tactic: obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_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⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
have mpr : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (x₂ : A₂ ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0) (y₁ : A₂ ⟶ S₂.X₁)
  (hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
Tactic: obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ 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
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
have mpr : (π₂ ≫ π₁) ≫ γ = CategoryStruct.comp (Y := S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) (homologyMap φ)
Tactic: refine ⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ (π₂ ≫ π₁) ≫ γ = CategoryStruct.comp (Y := S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) (homologyMap φ)
have mpr : ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
Tactic: simp only [assoc, fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
        I.cocomplex)
      (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Iso.inv (I.isoRightDerivedToHomotopyCategoryObj F) ≫ Functor.map F.rightDerivedToHomotopyCategory f)
    (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)) φ ≫
      Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))
have rw : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
    (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
  (Functor.map F.rightDerivedToHomotopyCategory f)
  (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F) ≫
    Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)) φ ≫
      Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))
Tactic: rw [← cancel_epi (I.isoRightDerivedToHomotopyCategoryObj F).hom, Iso.hom_inv_id_assoc]