awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SingleHomology
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
⊢ Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (CategoryStruct.comp (Y := cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j) (iCycles (Functor.obj (single C c j) B) j))
    ((Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B)) ≫
      iCycles (Functor.obj (single C c j) B) j)

Tactic:
simp only [cyclesMap_i, singleObjCyclesSelfIso, Iso.trans_hom, iCyclesIso_hom, Iso.trans_inv,
    assoc, iCyclesIso_inv_hom_id, comp_id, single_map_f_self]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.singleObjCyclesSelfIso, HomologicalComplex.iCyclesIso_inv_hom_id, CategoryTheory.Category.comp_id, HomologicalComplex.single_map_f_self, CategoryTheory.Iso.trans_hom, HomologicalComplex.cyclesMap_i, HomologicalComplex.iCyclesIso_hom, CategoryTheory.Iso.trans_inv
-- Module: Mathlib.Algebra.Homology.SingleHomology
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 (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.hom (singleObjCyclesSelfIso c j B) ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (cycles.{v, u, u_1} (Functor.obj (single C c j) B) j))
rw₄ rw₅ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
⊢ Eq (α := A ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Premises used: HomologicalComplex.singleObjCyclesSelfIso, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, HomologicalComplex.singleObjCyclesSelfIso_hom_naturality_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.SingleHomology
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 (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      homologyπ (Functor.obj (single C c j) B) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjCyclesSelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B) (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₄ rw₅ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B) (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
⊢ Eq (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)

Tactic:
rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_hom_assoc]

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.singleObjCyclesSelfIso_hom_naturality, HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc, HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj, HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.SingleHomology
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 :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
      (Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₁ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₂ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₃ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A)) (Iso.hom (singleObjHomologySelfIso c j A) ≫ f) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₄ :
  f =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₅ : f = f ≫ 𝟙 B
rw₆ rw₇ : f = f
⊢ Eq (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjHomologySelfIso c j B))

Tactic:
rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.singleObjHomologySelfIso_hom_naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
A : C
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
⊢ Eq (α := (mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f' g').obj' 2 _proof_247✝)
    ((mk₂ f g).map' 1 2 _proof_246✝ _proof_247✝ ≫ β.app 1) (α.app 1 ≫ (mk₂ f' g').map' 1 2 _proof_246✝ _proof_247✝)

Tactic:
simpa only [hαβ] using naturality' β 0 1

Premises used: CategoryTheory.ComposableArrows.naturality', OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
⊢ 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) ⋯ ⋯) ≫
      (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) ⋯ ⋯))

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')
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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'))
⊢ 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'))

Tactic:
h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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) ⋯
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')) →
    α = homMk₁ (α.app 0) (α.app 1) ⋯
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α

Tactic:
convert! h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
subst : X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) = 0
⊢ X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) = 0

Tactic:
(X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).zero 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₁', CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.Abelian.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) = 0

Tactic:
exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).zero 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₁', CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₀ : ℤ
subst : (X.H n₀).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) = 0
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) = 0

Tactic:
(X.exact₂' n₀ (mk₂ f g)).zero 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) = 0

Tactic:
exact (X.exact₂' n₀ (mk₂ f g)).zero 0

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
subst : (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) ≫ X.δ f g n₀ n₁ hn₁ = 0
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
(X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.Abelian.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
exact (X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
subst : (X.sc₁ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact
⊢ (X.sc₁ f g fg h n₀ n₁ hn₁).Exact

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact

Tactic:
(X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₁', CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.Abelian.SpectralObject.sc₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.Abelian.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.Exact.exact, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact

Tactic:
exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₁', CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₀ : ℤ
subst : (X.sc₂ f g (f ≫ g) ⋯ n₀).Exact
⊢ (X.sc₂ f g fg h n₀).Exact

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ : ℤ
⊢ (X.sc₂ f g (f ≫ g) ⋯ n₀).Exact

Tactic:
(X.exact₂' n₀ (mk₂ f g)).exact 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.ComposableArrows.Exact.exact, CategoryTheory.ComposableArrows.mk₁, CategoryTheory.Abelian.SpectralObject.sc₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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
n₀ : ℤ
⊢ (X.sc₂ f g (f ≫ g) ⋯ n₀).Exact

Tactic:
exact (X.exact₂' n₀ (mk₂ f g)).exact 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
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₁
subst : (X.sc₃ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact
⊢ (X.sc₃ f g fg h n₀ n₁ hn₁).Exact

Tactic:
subst h