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

Proof state:
case neg.inr.H.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : ¬m + 1 < q
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val✝ : ℕ
isLt✝ : val✝ < m + 1 + 1
hj₁ : m + 1 + 1 ≤ ↑⟨val✝, isLt✝⟩ + (q + 1)
hj₂ : ¬a = ↑⟨val✝, isLt✝⟩
haj : a < ↑⟨val✝, isLt✝⟩
⊢ ↑⟨a + 1, ⋯⟩ = ↑⟨val✝, isLt✝⟩.castSucc

Tactic:
dsimp

Result:
case neg.inr.H.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : ¬m + 1 < q
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val✝ : ℕ
isLt✝ : val✝ < m + 1 + 1
hj₁ : m + 1 + 1 ≤ ↑⟨val✝, isLt✝⟩ + (q + 1)
hj₂ : ¬a = ↑⟨val✝, isLt✝⟩
haj : a < ↑⟨val✝, isLt✝⟩
⊢ a + 1 = val✝

Proof state:
case neg.inr.H.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ ↑⟨a + 1, ⋯⟩ = ↑j.castSucc

Tactic:
cases j

Result:
case neg.inr.H.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : ¬m + 1 < q
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val✝ : ℕ
isLt✝ : val✝ < m + 1 + 1
hj₁ : m + 1 + 1 ≤ ↑⟨val✝, isLt✝⟩ + (q + 1)
hj₂ : ¬a = ↑⟨val✝, isLt✝⟩
haj : a < ↑⟨val✝, isLt✝⟩
⊢ ↑⟨a + 1, ⋯⟩ = ↑⟨val✝, isLt✝⟩.castSucc

Proof state:
case neg.inr.H.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : ¬m + 1 < q
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val✝ : ℕ
isLt✝ : val✝ < m + 1 + 1
hj₁ : m + 1 + 1 ≤ val✝ + (q + 1)
hj₂ : ¬a = val✝
haj : a < val✝
⊢ a + 1 = val✝

Tactic:
omega

Result:
no goals

Proof state:
case neg.inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Tactic:
simp only [← assoc, v j (by omega), zero_comp]

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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ ↑⟨a, ⋯⟩.succ < ↑j.succ

Tactic:
simpa only [Fin.val_mk, Fin.val_succ, add_lt_add_iff_right] using haj

Result:
no goals

Proof state:
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ⟨a + 1, ⋯⟩ ≤ j.castSucc

Tactic:
rw [Fin.le_iff_val_le_val]

Result:
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ↑⟨a + 1, ⋯⟩ ≤ ↑j.castSucc

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ ⟨a, ⋯⟩.succ < j.succ

Tactic:
rw [Fin.lt_iff_val_lt_val]

Result:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ ↑⟨a, ⋯⟩.succ < ↑j.succ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
⊢ a ≤ ↑j

Tactic:
omega

Result:
no goals

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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0

Tactic:
rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by omega)]

Result:
no goals

Proof state:
case neg.inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ (⟨a + 1, ⋯⟩.castLT ⋯) ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ⟨a + 1, ⋯⟩ ≤ j.castSucc

Tactic:
swap

Result:
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ⟨a + 1, ⋯⟩ ≤ j.castSucc

case neg.inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : ¬m + 1 < q
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ (⟨a + 1, ⋯⟩.castLT ⋯) ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Proof state:
case neg.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X _⦋0 + 1⦌
v : HigherFacesVanish q φ
j : Fin (0 + 1)
hj₁ : 0 + 1 ≤ ↑j + (q + 1)
hqn : ¬0 < q
ha : q + a = 0
⊢ φ ≫ X.δ (Fin.succ 0) = φ ≫ X.δ ⟨0 + 1, ⋯⟩

Tactic:
rfl

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 φ
⊢ HigherFacesVanish (q + 1) (φ ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q).f (n + 1))

Tactic:
intro j hj₁

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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q).f (n + 1)) ≫ X.δ j.succ = 0