awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂' :
  CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)
      (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) 0 (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)
hx₂'₁ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
have hx₂'₂ : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ sorry) n₂ = 0
Tactic: rw [assoc, zero_comp, X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃] at hx₂'
Cleared hypotheses: hx₂'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
  Epi π₁ →
    ∀ (x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) sorry f₃₄ h₃₄ n₁ n₂ sorry).sc sorry 1 sorry).X₁)
      (hx₁ :
        π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry = x₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) sorry f₃₄ h₃₄ n₁ n₂ sorry).sc sorry 1 sorry).f),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
        π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry
Tactic: obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    ((X.sequenceΨ_exact f₂ f₃ f₄ _ rfl f₃₄ h₃₄ n₁ n₂).exact 1).exact_up_to_refinements
      (x₂ ≫ X.ιE ..) (by simp [sequenceΨ, Precomp.map, hx₂'])
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
have refine : π₁ ≫ x₂ =
  CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
    (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
Tactic: refine ⟨A₁, π₁, inferInstance, x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw : (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry =
  CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry)
    (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry))
    (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry)
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry =
  CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry)
    (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry))
    (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry)
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₁ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw₂ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry =
  CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
    (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry))
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₁ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₂ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw₃ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry =
  x₁ ≫
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry))
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₁ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₂ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₃ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    x₁ ≫
      CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
          (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw₄ : x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ sorry =
  x₁ ≫
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry))
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₁ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₂ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₃ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    x₁ ≫
      CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
          (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₄ :
  x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯ =
    x₁ ≫
      CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
          (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
have rw₅ : x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ sorry = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ sorry
Tactic: rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ sorry sorry sorry).X₂),
  x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ sorry sorry sorry).g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ sorry sorry sorry).X₁),
      π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ sorry sorry sorry).f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
    π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f
have dsimp : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
  π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry
Tactic: dsimp at hx₂ ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
  Epi π₁ →
    ∀ (y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁) (hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
        π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry
Tactic: obtain ⟨A₁, π₁, _, y₂, hy₂⟩ :=
    surjective_up_to_refinements_of_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂) x₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
have hy₂' : (π₁ ≫ x₂) ≫
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) =
  CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) (y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry)
    (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry)
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry))
Tactic: have hy₂' := hy₂ =≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ≫ X.ιE ..
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' :
  (π₁ ≫ x₂) ≫
      CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
have hy₂'₁ : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ sorry
Tactic: simp only [assoc, reassoc_of% hx₂, zero_comp, comp_zero, πE_d_ιE] at hy₂'
Cleared hypotheses: hy₂'