case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = φ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
induction' q with q hq
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ
simp only [P_zero]
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ
apply comp_id
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = φ
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
  comp_id, ← assoc, hq v.of_succ, add_right_eq_self]
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
by_cases hqn : n < q
no goals
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
. obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
  have hnaq : n = a + q := by linarith
  simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
  have eq := v ⟨a, by linarith⟩ (by
    simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
    rfl)
  simp only [Fin.succ_mk] at eq
  simp only [eq, zero_comp]
no goals
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
exact v.of_succ.comp_Hσ_eq_zero hqn
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
have hnaq : n = a + q := by linarith
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X (Fin.succ { val := a, isLt := (_ : a < n + 1) }) = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
have eq := v ⟨a, by linarith⟩ (by
  simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
  rfl)
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X (Fin.succ { val := a, isLt := (_ : a < n + 1) }) = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
simp only [Fin.succ_mk] at eq
no goals
case neg.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
simp only [eq, zero_comp]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ n = a + q
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a < n + 1
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ ↑{ val := a, isLt := (_ : a < n + 1) } + Nat.succ q
simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj [n + 1].op
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)
rfl