awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
refine_1 :
  parallelPair (Y := (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯).pt)
      (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0 ≅
    parallelPair (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) 0
⊢ IsLimit (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯)
have refine_2 : (Cone.postcompose
        (parallelPair.ext
            (Iso.refl
              ((parallelPair (Y := (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry).pt)
                    (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry)) 0).obj
                WalkingParallelPair.zero))
            (Iso.refl
              ((parallelPair (Y := (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry).pt)
                    (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry)) 0).obj
                WalkingParallelPair.one))
            sorry sorry).hom).obj
    (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry)) sorry) ≅
  Fork.ofι (P := kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry)) (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry)) sorry
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f
have dsimp : Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g
have dsimp : Epi (Y := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂),
  x₂ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
      π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
  Epi π₁ →
    ∀ (y₁ : A₁ ⟶ (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₁)
      (hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).f),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
        π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: obtain ⟨A₁, π₁, _, y₁, hy₁⟩ :=
    (X.cokernelSequenceCyclesE_exact f₁ f₂ f₃ n₀ n₁ n₂).exact_up_to_refinements
      (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (by simpa using hx₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (hypothesis)
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₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
⊢ z ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).g = 0
have this : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
Tactic: have : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0 := by simp [z, hy₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
have obtain : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
  Epi π₂ →
    ∀ (x₁ : A₂ ⟶ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).X₁) (hx₁ : π₂ ≫ z = x₁ ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).f),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
        π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: obtain ⟨A₂, π₂, _, x₁, hx₁⟩ := (X.exact₂ f₁ f₂ f₁₂ h₁₂ n₁).exact_up_to_refinements z (by
      have : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0 := by simp [z, hy₁]
      simpa only [zero_comp, Category.assoc, toCycles_i] using this =≫ X.iCycles f₁ f₂ n₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂ = x
have dsimp : X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ sorry.desc x sorry = x
Tactic: dsimp only [descE]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ ⋯.desc x ⋯ = x
have rw : (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) ≫ sorry.desc x sorry = x
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
    0
have h₀ : Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f₃))
  (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ sorry))
    biprod.fst)
  (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁))) 0 biprod.fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₀ :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f₃))
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
      ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
      biprod.fst)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁))) 0 biprod.fst)
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
    0
have h₁ : Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ (X.H n₂).obj (mk₁ f₁))
  (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ sorry))
    biprod.snd)
  (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁))) 0 biprod.snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
have dsimp : Mono (X := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂),
  x₂ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁),
      π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = 0
have dsimp : X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ sorry ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ = 0
have rw : x₂ ≫ X.δ f₁ f₂₃ n₁ n₂ sorry = 0
Tactic: rw [← X.fromOpcyles_δ f₁ f₂ f₃ f₂₃ h₂₃ n₁ n₂,
          X.liftOpcycles_fromOpcycles_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
  Epi π₁ →
    ∀ (x₁ : A₁ ⟶ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁)
      (hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ sorry = x₁ ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁),
        π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    (X.kernelSequenceOpcyclesE_exact f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).exact_up_to_refinements
      (X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ (by simpa using hx₂ =≫ biprod.fst)) (by
        dsimp
        rw [← X.fromOpcyles_δ f₁ f₂ f₃ f₂₃ h₂₃ n₁ n₂,
          X.liftOpcycles_fromOpcycles_assoc]
        simpa using hx₂ =≫ biprod.snd)
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
have refine : π₁ ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: refine ⟨A₁, π₁, inferInstance, x₁, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
⊢ π₁ ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
have dsimp : π₁ ≫ x₂ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
⊢ π₁ ≫ x₂ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
have rw : π₁ ≫ x₂ = π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ sorry ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
Tactic: rw [← reassoc_of% hx₁, liftOpcycles_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ :
  Eq (α := A ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    (x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
rw : π₁ ≫ x₂ = π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
⊢ π₁ ≫ x₂ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
have rw₁ : π₁ ≫ x₂ = π₁ ≫ x₂
Tactic: rw [← reassoc_of% hx₁, liftOpcycles_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
hβ : β = homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv ≫
      ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) =
    X.cyclesMap f₁ f₂ f₁' f₂' β n₁ ≫ (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv
have subst : (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv ≫
    ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) =
  X.cyclesMap f₁ f₂ f₁' f₂' (homMk₂ (α.app 0) (α.app 1) (α.app 2) sorry sorry) n₁ ≫
    (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv
Tactic: subst hβ
Cleared hypotheses: β, hβ
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
γ : mk₂ f₂ f₃ ⟶ mk₂ f₂' f₃'
hγ : γ = homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) ≫
      (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁
have subst : ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) ≫
    (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom =
  (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫
    X.opcyclesMap f₂ f₃ f₂' f₃' (homMk₂ (α.app 1) (α.app 2) (α.app 3) sorry sorry) n₁
Tactic: subst hγ
Cleared hypotheses: γ, hγ
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g
have dsimp : Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂),
  x₂ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
      π ≫ x₂ = x₁ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]