awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
rw₁ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    0
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw₂ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
  ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry) ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) 0
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
rw₁ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    0
rw₂ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) 0
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw₃ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
  ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry) ≫ X.δ f₁ f₂₃ n₀ n₁ sorry ≫ X.pOpcycles f₁ f₂ n₁) 0
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
rw₁ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    0
rw₂ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) 0
rw₃ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁) 0
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw₄ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁) (0 ≫ X.pOpcycles f₁ f₂ n₁) 0
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
rw₁ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    0
rw₂ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) 0
rw₃ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁) 0
rw₄ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁) (0 ≫ X.pOpcycles f₁ f₂ n₁) 0
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw₅ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁) 0 0
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
  ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
    X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry n₁)
  (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry n₁)
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₁ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
  ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
    X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry n₁)
  0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₂ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
  (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
    X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) sorry n₁)
  0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₂ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₃ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
  (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) sorry)) 0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₂ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₃ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₄ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
  (X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ sorry ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) sorry)) 0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₂ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₃ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
rw₄ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₅ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃))) (X.iCycles f₂ f₃ n₀ ≫ 0) 0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₂ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₃ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
rw₄ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
rw₅ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃))) (X.iCycles f₂ f₃ n₀ ≫ 0) 0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
have rw₆ : Eq.{v_1 + 1} (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃))) 0 0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
      f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact
have rw : ∀ ⦃A : C⦄
  (x₂ :
    A ⟶
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := sorry :
          ShortComplex.{v_1, u_1} C }.X₂),
  x₂ ≫
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := sorry :
            ShortComplex.{v_1, u_1} C }.g =
      0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
      A' ⟶
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := sorry :
            ShortComplex.{v_1, u_1} C }.X₁),
      π ≫ x₂ =
        x₁ ≫
          { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
              f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              zero := sorry }.f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z =
      x₁ ≫
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f
have refine_1 : (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0
Tactic: refine ⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_1 : (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z =
      x₁ ≫
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f
have refine_2 : 𝟙 A ≫ z =
  X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) sorry ≫
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := sorry }.f
Tactic: refine ⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩