-- Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1)) (hi : n + 1 ≤ i + q) :
    X.σ i ≫ (P q).f (n + 1) = 0

Proof state:
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ ⟨↑i, ⋯⟩ ≤ j.rev

Tactic:
simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val, Fin.val_mk]

Result:
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ ↑i ≤ k

Proof state:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies._hyg.310.«0»
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 1).f 1 = 0

Tactic:
simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
  HomologicalComplex.id_f, AlternatingFaceMapComplex.obj_d_eq, Hσ,
  HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
  comp_id]

Result:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies._hyg.310.«0»
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i : Fin (0 + 2), (-1) ^ ↑i • X.δ i) ≫ hσ' 0 0 1 ⋯ +
        X.σ 0 ≫ (P 0).f 1 ≫ hσ' 0 1 2 ⋯ ≫ ∑ i : Fin (1 + 2), (-1) ^ ↑i • X.δ i) =
    0

Proof state:
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
have hi' : i = Fin.castSucc ⟨i, by omega⟩ := by
  ext
  simp only [Fin.castSucc_mk, Fin.eta]

Result:
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
⊢ (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Proof state:
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (n + 1 + 1) = 0

Tactic:
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
  P_succ]

Result:
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) +
      ((Q q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) =
    0

Proof state:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies._hyg.310.«0»
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i : Fin (0 + 2), (-1) ^ ↑i • X.δ i) ≫ hσ' 0 0 1 ⋯ +
        X.σ 0 ≫ (P 0).f 1 ≫ hσ' 0 1 2 ⋯ ≫ ∑ i : Fin (1 + 2), (-1) ^ ↑i • X.δ i) =
    0

Tactic:
rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]

Result:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies._hyg.310.«0»
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i : Fin (0 + 2), (-1) ^ ↑i • X.δ i) ≫ ((-1) ^ 0 • X.σ ⟨0, ⋯⟩) +
        X.σ 0 ≫ (P 0).f 1 ≫ ((-1) ^ 1 • X.σ ⟨1, ⋯⟩) ≫ ∑ i : Fin (1 + 2), (-1) ^ ↑i • X.δ i) =
    0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + 0 → X.σ i ≫ (P 0).f (n + 1) = 0

Tactic:
intro i (hi : n + 1 ≤ i)

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i
⊢ X.σ i ≫ (P 0).f (n + 1) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q
⊢ X.σ i ≫ (P q).f (n + 1) = 0

Tactic:
revert i hi

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
⊢ ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0

Proof state:
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) +
      ((Q q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) =
    0

Tactic:
have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
  (HigherFacesVanish.of_P q n).comp_σ hi

Result:
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) +
      ((Q q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) =
    0

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
⊢ ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + (q + 1) → X.σ i ≫ (P (q + 1)).f (n + 1) = 0

Tactic:
intro i (hi : n + 1 ≤ i + q + 1)

Result:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
⊢ X.σ i ≫ (P (q + 1)).f (n + 1) = 0