Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: case e'_2.e'_6.e'_8
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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αβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((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'))
e_3✝ : (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯))
e_4✝ : (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯))
e_6✝ : mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)
e_7✝ : mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯)
⊢ β = homMk₁ (α.app 1) (β.app 1) ⋯

pp: case e'_3.e'_7
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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αβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((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) ⋯

Tactic:
<;>

Goal state after:
case e'_2.e'_6.e'_8
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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αβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((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'))
e_3✝ : (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯))
e_4✝ : (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯))
e_6✝ : mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)
e_7✝ : mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯)
⊢ β = homMk₁ (α.app 1) (β.app 1) ⋯

case e'_3.e'_7
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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αβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((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) ⋯