-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + q
zero :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + 0),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P 0) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ :
  ∀ (q : ℕ)
    (hq :
      ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
        Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
          (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)))
    (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + (q + 1)),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
induction q generalizing i with
  | zero => lia
  | succ q hq =>
    by_cases h : n + 1 ≤ (i : ℕ) + q
    · rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
    · replace hi : n = i + q := by lia
      rcases n with _ | n
      · fin_cases i
        dsimp at h hi
        rw [show q = 0 by lia]
        change X.σ 0 ≫ (P 1).f 1 = 0
        simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]
        rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]
        dsimp [P_zero]
        rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]
        rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
        simp only [add_neg_cancel, add_zero, zero_add]
      · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]
        have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
        dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]
        rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]
        intro j hj
        simp only [Finset.mem_univ, Finset.mem_filter] at hj
        obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
        rw [add_comm] at hk
        have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
        have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
        rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]
        simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]
        lia

Premises used: Finset.mem_univ, CategoryTheory.Category.assoc, add_neg_cancel, neg_smul, add_neg_eq_zero, Nat.succ_eq_add_one, HomologicalComplex.add_f_apply, HomologicalComplex.Hom.f, Fin.castSucc_one, Finset.sum_eq_zero, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, pow_add, HomologicalComplex.id_f, Fin.isLt, CategoryTheory.Preadditive.sum_comp, neg_neg, Fin.val_one, Fin.val_succ, Fin.eta, AlgebraicTopology.DoldKan.Hσ, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, Fin.succ_zero_eq_one, HomologicalComplex.comp_f, Fin.val, zero_add, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, add_comm, pow_zero, one_smul, Fin.succ_mk, CategoryTheory.Preadditive.add_comp, CategoryTheory.SimplicialObject.δ_comp_σ_of_le, CategoryTheory.SimplicialObject.δ_comp_σ_self, Fin.castSucc_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ, AlgebraicTopology.DoldKan.c_mk, pow_one, CategoryTheory.Preadditive.comp_add, CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc, CategoryTheory.Preadditive.neg_comp, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.SimplicialObject.σ_comp_σ_assoc, Finset.mem_filter, neg_mul, CategoryTheory.Limits.zero_comp, Homotopy.nullHomotopicMap'_f, AlgebraicTopology.DoldKan.decomposition_Q, add_zero, Fin.sum_univ_two, OfNat.ofNat, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, Eq.symm, Nat.succ, Fin.val_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, AlgebraicTopology.DoldKan.hσ'_eq', one_mul, rfl, mul_neg, Fin.sum_univ_succ, CategoryTheory.Category.id_comp, CategoryTheory.SimplicialObject.σ, Fin.le_iff_val_le_val, AlgebraicTopology.DoldKan.P