Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₁

pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₂

pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₃

Tactic:
<;>

Goal state after:
case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₁

case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₂

case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₃