awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₁ : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
    Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
  ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₂ : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
    Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
  (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₃ : opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
    𝟙 (opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j) =
  Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B)
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j) =
    Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B)
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₄ : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j) =
    Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B)
rw₄ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₅ : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫
    Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j) =
    Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B)
rw₄ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₅ :
  Eq (α :=
    opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw₆ : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : Eq (α := (mk₁ f).obj 1 ⟶ (mk₁ f').obj 1) (α.app 1) (β.app 0)
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α
have h : Eq (α :=
  (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.H n₀).obj (mk₂ f g) ⟶
    (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.H n₁).obj (mk₂ f' g'))
  ((functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.H n₀).map (homMk₂ (α.app 0) (α.app 1) (β.app 1) sorry sorry) ≫
    (X.δ' n₀ n₁ hn₁).app (mk₂ f' g'))
  ((X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫
    (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.H n₁).map (homMk₂ (α.app 0) (α.app 1) (β.app 1) sorry sorry))
Tactic: have h := (X.δ' n₀ n₁ hn₁).naturality
    (homMk₂ (α.app 0) (α.app 1) (β.app 1) (naturality' α 0 1)
      (by simpa only [hαβ] using naturality' β 0 1) : mk₂ f g ⟶ mk₂ f' g')
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : Eq (α := (mk₁ f).obj 1 ⟶ (mk₁ f').obj 1) (α.app 1) (β.app 0)
hn₁ : n₀ + 1 = n₁
h :
  Eq (α := (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
    ((X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') :
      (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
    ((X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯) :
      (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α
have h₁ : ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 sorry)) ⟶ (X.H n₁).obj (mk₁ f')) →
  (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 sorry)) →
    (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 sorry)) →
      mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 sorry) →
        mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 sorry) → β = homMk₁ (α.app 1) (β.app 1) sorry
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : Eq (α := (mk₁ f).obj 1 ⟶ (mk₁ f').obj 1) (α.app 1) (β.app 0)
hn₁ : n₀ + 1 = n₁
h :
  Eq (α := (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
    ((X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') :
      (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
    ((X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯) :
      (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
h₁ :
  ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
      ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f')) →
    (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) →
      (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯)) →
        mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯) →
          mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯) → β = homMk₁ (α.app 1) (β.app 1) ⋯
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α
have h₂ : ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 sorry)) ⟶ (X.H n₁).obj (mk₁ f')) →
  α = homMk₁ (α.app 0) (α.app 1) sorry
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0
have subst : X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g (f ≫ g) sorry) = 0
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0
have subst : (X.H n₀).map (twoδ₂Toδ₁ f g (f ≫ g) sorry) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) sorry) = 0
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n₀ n₁ hn₁ = 0
have subst : (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) sorry) ≫ X.δ f g n₀ n₁ hn₁ = 0
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g fg h n₀ n₁ hn₁).Exact
have subst : (X.sc₁ f g (f ≫ g) sorry n₀ n₁ hn₁).Exact
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.sc₂ f g fg h n₀).Exact
have subst : (X.sc₂ f g (f ≫ g) sorry n₀).Exact
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₃ f g fg h n₀ n₁ hn₁).Exact
have subst : (X.sc₃ f g (f ≫ g) sorry n₀ n₁ hn₁).Exact
Tactic: subst h
Cleared hypotheses: fg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
have eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) sorry) ≫ X.δ f (g ≫ h) n₁ n₂ sorry = X.δ f g n₁ n₂ sorry ≫ (X.H n₂).map (𝟙 (mk₁ f))
Tactic: have eq := X.δ_naturality f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl) n₁ n₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯ ≫ (X.H n₂).map (𝟙 (mk₁ f))
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
have eq₁ : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) sorry) ≫ X.δ f (g ≫ h) n₁ n₂ sorry = X.δ f g n₁ n₂ sorry
Tactic: rw [Functor.map_id, comp_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
have rw : X.δ g h n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) sorry) ≫ X.δ f (g ≫ h) n₁ n₂ sorry = 0
Tactic: rw [← eq, X.zero₁_assoc g h _ rfl n₀ n₁ hn₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
rw : X.δ g h n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = 0
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
have rw₁ : Eq (α := (X.H n₀).obj (mk₁ h) ⟶ (X.H n₂).obj (mk₁ f)) (0 ≫ X.δ f (g ≫ h) n₁ n₂ sorry) 0
Tactic: rw [← eq, X.zero₁_assoc g h _ rfl n₀ n₁ hn₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
rw : X.δ g h n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = 0
rw₁ : Eq (α := (X.H n₀).obj (mk₁ h) ⟶ (X.H n₂).obj (mk₁ f)) (0 ≫ X.δ f (g ≫ h) n₁ n₂ ⋯) 0
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
have rw₂ : Eq.{u_4 + 1} (α := (X.H n₀).obj (mk₁ h) ⟶ (X.H n₂).obj (mk₁ f)) 0 0
Tactic: rw [← eq, X.zero₁_assoc g h _ rfl n₀ n₁ hn₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso φ
have rw : IsIso (X := (mk₁ f).obj 0) (φ.app 0) ∧ IsIso (X := (mk₁ f).obj 1) (φ.app 1)
Tactic: rw [isIso_iff₁]