-- 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:
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
h : ¬n + 1 ≤ ↑i + q
⊢ n = ↑i + q

Tactic:
obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi

Result:
case intro
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
h : ¬n + 1 ≤ ↑i + q
j : ℕ
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q

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
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

Tactic:
dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
  HomologicalComplex.add_f_apply, HomologicalComplex.id_f]

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 + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (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) ≫ ((-1) ^ 0 • X.σ ⟨0, ⋯⟩) +
        X.σ 0 ≫ (P 0).f 1 ≫ ((-1) ^ 1 • X.σ ⟨1, ⋯⟩) ≫ ∑ i : Fin (1 + 2), (-1) ^ ↑i • X.δ i) =
    0

Tactic:
dsimp [P_zero]

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 ≫ 𝟙 (X _⦋1⦌) +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (∑ i : Fin 2, (-1) ^ ↑i • X.δ i) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i : Fin 3, (-1) ^ ↑i • X.δ i) =
    0

Proof state:
case intro
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
h : ¬n + 1 ≤ ↑i + q
j : ℕ
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q

Tactic:
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right,
  nonpos_iff_eq_zero] at h

Result:
case intro
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
j : ℕ
h : j = 0
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q

Proof state:
case neg
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
h : ¬n + 1 ≤ ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (n + 1) = 0

Tactic:
replace hi : n = i + q := by
  obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right,
    nonpos_iff_eq_zero] at h
  rw [← add_left_inj 1, hj, self_eq_add_right, h]

Result:
case neg
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)
h : ¬n + 1 ≤ ↑i + q
hi : n = ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (n + 1) = 0

Proof state:
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
⊢ ↑i < n + 1

Tactic:
omega

Result:
no goals

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
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ (((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:
rw [assoc, assoc, assoc, hi',
  SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
  comp_zero]

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, ⋯⟩ ≤ j.rev