awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
h₂ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
h₃ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    ShortComplex.Hom.τ₃ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
⊢ X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  (X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) ⋯) =
    𝟙 ((X.H n₀).obj (mk₁ f₃))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
⊢ (X.H n₀).map (𝟙 (mk₁ f₃)) = 𝟙 ((X.H n₀).obj (mk₁ f₃))

Tactic:
(X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h : homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) ⋯ = 𝟙 (mk₁ f₃)
⊢ (X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) ⋯) =
    𝟙 ((X.H n₀).obj (mk₁ f₃))

Tactic:
convert! (X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₂ : (X.H n₁).map (homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) ⋯) = 𝟙 ((X.H n₁).obj (mk₁ f₂))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
⊢ (X.H n₁).map (𝟙 (mk₁ f₂)) = 𝟙 ((X.H n₁).obj (mk₁ f₂))

Tactic:
(X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h : homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) ⋯ = 𝟙 (mk₁ f₂)
⊢ (X.H n₁).map (homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) ⋯) = 𝟙 ((X.H n₁).obj (mk₁ f₂))

Tactic:
convert! (X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₃ : (X.H n₂).map (homMk₁ (𝟙 i) (𝟙 j) ⋯) = 𝟙 ((X.H n₂).obj (mk₁ f₁))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    ShortComplex.Hom.τ₃ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
⊢ (X.H n₂).map (𝟙 (mk₁ f₁)) = 𝟙 ((X.H n₂).obj (mk₁ f₁))

Tactic:
(X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h : homMk₁ (𝟙 i) (𝟙 j) ⋯ = 𝟙 (mk₁ f₁)
⊢ (X.H n₂).map (homMk₁ (𝟙 i) (𝟙 j) ⋯) = 𝟙 ((X.H n₂).obj (mk₁ f₁))

Tactic:
convert! (X.H _).map_id _

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁
h₂ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂
h₃ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₃
⊢ X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₀).obj (mk₁ f₃')) ((X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯))
      ((X.H n₀).map (homMk₁ (β.app 2) (β.app 3) ⋯)))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    ((X.H n₀).map (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) ⋯) (homMk₁ (β.app 2) (β.app 3) ⋯)))
⊢ Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₀).obj (mk₁ f₃')) ((X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯))
      ((X.H n₀).map (homMk₁ (β.app 2) (β.app 3) ⋯)))

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₁ :
  Eq.{v_2 + 1} (α := mk₁ f₃ ⟶ mk₁ f₃'')
    (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯)
    (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) ⋯) (homMk₁ (β.app 2) (β.app 3) ⋯))
⊢ Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    ((X.H n₀).map (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) ⋯) (homMk₁ (β.app 2) (β.app 3) ⋯)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₂ :
  Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f₂')) ((X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯))
      ((X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₂ :
  Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    ((X.H n₁).map (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (β.app 1) (β.app 2) ⋯)))
⊢ Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f₂')) ((X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯))
      ((X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)))

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₂ :
  Eq.{v_2 + 1} (α := mk₁ f₂ ⟶ mk₁ f₂'')
    (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯)
    (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (β.app 1) (β.app 2) ⋯))
⊢ Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    ((X.H n₁).map (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (β.app 1) (β.app 2) ⋯)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₃ :
  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))
        ⋯))
    (CategoryStruct.comp (Y := (X.H n₂).obj (mk₁ f₁')) ((X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯))
      ((X.H n₂).map (homMk₁ (β.app 0) (β.app 1) ⋯)))
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
h₃ :
  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) ⋯)))
⊢ 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))
        ⋯))
    (CategoryStruct.comp (Y := (X.H n₂).obj (mk₁ f₁')) ((X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯))
      ((X.H n₂).map (homMk₁ (β.app 0) (β.app 1) ⋯)))

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
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)) ⋯)
    (CategoryStruct.comp (Y := mk₁ f₁') (homMk₁ (α.app 0) (α.app 1) ⋯) (homMk₁ (β.app 0) (β.app 1) ⋯))
⊢ 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) ⋯)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
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₂ ⋯ ⋯).homology) (𝟙 (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂))
⊢ 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₂)

Tactic:
simp [shortComplexMap_id, ShortComplex.homologyMap_id]

Premises used: CategoryTheory.Abelian.SpectralObject.shortComplexMap_id, CategoryTheory.ShortComplex.homologyMap_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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.{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₂ ⋯ ⋯).homology) (𝟙 (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₂
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₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ ⋯ ⋯).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₂ ⋯ ⋯) :
          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).homology)
        (ShortComplex.homologyMap (X.shortComplexMap f₁' f₂' f₃' 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.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₂

Tactic:
dsimp only [map]

Premises used: CategoryTheory.Abelian.SpectralObject.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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.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₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ ⋯ ⋯).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₂ ⋯ ⋯) :
          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).homology)
        (ShortComplex.homologyMap (X.shortComplexMap f₁' f₂' f₃' 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₂)

Tactic:
simp [shortComplexMap_comp, ShortComplex.homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp