-- Mathlib/AlgebraicTopology/DoldKan/Faces.lean
theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ)
    (hqn : n < q) : φ ≫ (Hσ q).f (n + 1) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Tactic:
by_cases hqn' : n + 1 < q

Result:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Proof state:
case neg.hf.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ 1 + ↑j + q

Tactic:
omega

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ X.σ 0 ≫ ((-1) ^ 0 • X.δ ⟨0, ⋯⟩) + φ ≫ X.σ 0 ≫ ((-1) ^ 1 • X.δ ⟨1, ⋯⟩) = 0

Tactic:
simp only [Fin.mk_zero, Fin.val_zero, pow_zero, one_zsmul, Fin.mk_one, Fin.val_one, pow_one,
  neg_smul, comp_neg]

Result:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ X.σ 0 ≫ X.δ 0 + -φ ≫ X.σ 0 ≫ X.δ 1 = 0

Proof state:
case neg.hf.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ ↑(Fin.succ 0) < 2 + ↑j

Tactic:
dsimp [Fin.succ]

Result:
case neg.hf.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ 1 < 2 + ↑j

Proof state:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Tactic:
rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ 2 + (n + 1) = n + 1 + 2

Tactic:
omega

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ ∑ j : Fin (n + 1 + 2), φ ≫ X.σ 0 ≫ ((-1) ^ ↑j • X.δ j) = 0

Tactic:
rw [← Fin.sum_congr' _ (show 2 + (n + 1) = n + 1 + 2 by omega), Fin.sum_trunc]

Result:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ ∑ i : Fin 2, φ ≫ X.σ 0 ≫ ((-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ i)) • X.δ (Fin.cast ⋯ (Fin.castLE ⋯ i))) = 0

case neg.hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ ∀ (j : Fin (n + 1)), φ ≫ X.σ 0 ≫ ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd 2 j)) • X.δ (Fin.cast ⋯ (Fin.natAdd 2 j))) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫
      ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ hσ' q n (n + 1) ⋯ +
        hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) =
    0