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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₂).obj (mk₁ f₁) ⟶ (X.H n₂).obj (mk₁ f₁''))
    ((X.H n₂).map
      (homMk₁ (CategoryStruct.comp (Y := i') (α.app 0) (β.app 0)) (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        ⋯))
    ((X.H n₂).map (CategoryStruct.comp (Y := mk₁ f₁') (homMk₁ (α.app 0) (α.app 1) ⋯) (homMk₁ (β.app 0) (β.app 1) ⋯)))
have h₃ : Eq.{v_2 + 1} (α := mk₁ f₁ ⟶ mk₁ f₁'')
  (homMk₁ (CategoryStruct.comp (Y := i') (α.app 0) (β.app 0)) (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1)) sorry)
  (CategoryStruct.comp (Y := mk₁ f₁') (homMk₁ (α.app 0) (α.app 1) sorry) (homMk₁ (β.app 0) (β.app 1) sorry))
Tactic: congr 1
-- 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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
    (ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology)
    (𝟙 (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
have simp : Eq.{v_1 + 1} (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
  (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).homology) (𝟙 (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂))
Tactic: simp [shortComplexMap_id, ShortComplex.homologyMap_id]
-- 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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫ X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂
have dsimp : Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁'' f₂'' f₃'' n₀ n₁ n₂ hn₁ hn₂)
  (ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).homology ⟶ (X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ sorry sorry).homology)
  (CategoryStruct.comp (Y := X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂)
      (ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ sorry sorry) :
        (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).homology ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).homology)
      (ShortComplex.homologyMap (X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ sorry sorry) :
        (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).homology ⟶ (X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ sorry sorry).homology) :
    X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁'' f₂'' f₃'' n₀ n₁ n₂ hn₁ hn₂)
Tactic: dsimp only [map]
-- 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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
have inst : IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₁) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₁)
  (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₁ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₁)
Tactic: apply +allowSynthFailures ShortComplex.isIso_of_isIso
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
inst_3 : 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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
inst :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
⊢ IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
have inst₁ : IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₂) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₂)
  (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₂ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₂)
Tactic: apply +allowSynthFailures ShortComplex.isIso_of_isIso
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
inst_3 : 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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
inst :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
inst₁ :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)
⊢ IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
have inst₂ : IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₃) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₃)
  (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).X₃ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry).X₃)
Tactic: apply +allowSynthFailures ShortComplex.isIso_of_isIso
-- 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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
have this : IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry)
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ sorry sorry :
    X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ sorry sorry)
Tactic: have : IsIso (shortComplexMap X f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂) := by
    apply +allowSynthFailures ShortComplex.isIso_of_isIso <;> assumption
-- 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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))
have refine : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))
Tactic: refine IsZero.of_iso ?_ ((X.H n).mapIso e.symm)
-- 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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))
have h : Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
  ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) sorry) ≫ (X.H n).map (twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) sorry)) 0
Tactic: have h := X.zero₂ (𝟙 i) (𝟙 i) (𝟙 i) (by simp) n
-- 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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))
have h₁ : Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
  ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) sorry ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) sorry)) 0
Tactic: rw [← Functor.map_comp] at 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 j : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))
have rw : (X.H n).map (𝟙 (mk₁ (𝟙 i))) = (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) sorry ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) sorry)
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← 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 j : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
⊢ (X.H n).map (𝟙 (mk₁ (𝟙 i))) = (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)
have e_a : Eq.{v_2 + 1} (α := Quiver.Hom (V := ComposableArrows.{v_2, u_2} ι 1) (mk₁ (𝟙 i)) (mk₁ (𝟙 i))) (𝟙 (mk₁ (𝟙 i)))
  (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) sorry ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) sorry)
Tactic: congr 1
-- 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₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData
have this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry).f sorry) = X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry
Tactic: have : hi.lift (KernelFork.ofι _ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).zero) =
      X.δToCycles f₁ f₂ f₃ n₀ n₁ :=
    Fork.IsLimit.hom_ext hi (by simpa using hi.fac _ .zero)
-- 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₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ Eq (α := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt ⟶ cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯) ≫
      cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    0
have rw : Eq (α := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry).pt ⟶ cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry))
  (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry)) 0
Tactic: rw [this]
-- 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₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯)
have refine_1 : parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry).pt)
    (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry)) 0 ≅
  parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry) 0
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (cokernelIsCokernel (X.δToCycles 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₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
refine_1 :
  parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
      (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0 ≅
    parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯)
have refine_2 : (Cocone.precompose
        (parallelPair.ext
            (Iso.refl
              ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry).pt)
                    (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry)) 0).obj
                WalkingParallelPair.zero))
            (Iso.refl
              ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry).pt)
                    (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f sorry)) 0).obj
                WalkingParallelPair.one))
            sorry sorry).inv).obj
    (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry)) sorry) ≅
  Cofork.ofπ (P := cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry)) (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ sorry)) sorry
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (cokernelIsCokernel (X.δToCycles 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₂
⊢ Epi (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g
have dsimp : Epi (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
Tactic: dsimp
-- 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₁₂
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
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).RightHomologyData
have this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
Tactic: have : hp.desc (CokernelCofork.ofπ _ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).zero) =
      X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ :=
    Cofork.IsColimit.hom_ext hp (by simpa using hp.fac _ .one)
-- 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₂
⊢ Eq (α :=
    kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) ⟶ (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯).pt)
    (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) ≫
      hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯))
    0
have rw : Eq (α :=
  kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry) ⟶ (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g sorry).pt)
  (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry) ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) 0
Tactic: rw [this]
-- 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₂
⊢ IsLimit (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯)
have refine_1 : 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 ≅
  parallelPair (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ sorry) 0
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))