-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem comp_P_eq_self {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) :
    φ ≫ (P q).f (n + 1) = φ

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

Tactic:
by_cases hqn : n < q

Result:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

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

Tactic:
obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)

Result:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ (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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ n = a + q

Tactic:
omega

Result:
no goals

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

Tactic:
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]

Result:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

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

Tactic:
have hnaq : n = a + q := by omega

Result:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (𝟙 K[X]).f (n + 1) = φ

Tactic:
apply comp_id

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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
exact v.of_succ.comp_Hσ_eq_zero hqn

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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ ↑⟨a, ⋯⟩ + (q + 1)

Tactic:
simp only [hnaq, Nat.succ_eq_add_one, add_assoc]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ φ ≫ (P (q + 1)).f (n + 1) = φ

Tactic:
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
  comp_id, ← assoc, hq v.of_succ, add_right_eq_self]

Result:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Proof state:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a + 1, ⋯⟩ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Tactic:
simp only [eq, zero_comp]

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 φ
⊢ φ ≫ (P q).f (n + 1) = φ

Tactic:
induction' q with q hq

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (P 0).f (n + 1) = φ

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ φ ≫ (P (q + 1)).f (n + 1) = φ

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

Tactic:
simp only [P_zero]

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (𝟙 K[X]).f (n + 1) = φ

Proof state:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Tactic:
have eq := v ⟨a, by omega⟩ (by
  simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
  rfl)

Result:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a, ⋯⟩.succ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a < n + 1

Tactic:
omega

Result:
no goals