[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f (P Nat.zero) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
rfl
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P (Nat.succ q)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f, HomologicalComplex.id_f, id_comp, hq,
  Hσ_eq_zero, add_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + Q q = 𝟙 K[X]
[PROOFSTEP]
rw [Q]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q (q + 1) = Q q - P q ≫ Hσ q
[PROOFSTEP]
simp only [Q, P_succ, comp_add, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (Q q) 0 = 0
[PROOFSTEP]
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
⊢ HomologicalComplex.Hom.f (P 0) (n + 1) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
exfalso
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
⊢ False
[PROOFSTEP]
have hj₂ := Fin.is_lt j
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
hj₂ : ↑j < n + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) (HomologicalComplex.Hom.f (P (q + 1)) (n + 1))
[PROOFSTEP]
simp only [P_succ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) (HomologicalComplex.Hom.f (P q ≫ (𝟙 K[X] + Hσ q)) (n + 1))
[PROOFSTEP]
exact (of_P q n).induction
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v : HigherFacesVanish q φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ
[PROOFSTEP]
simp only [P_zero]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1) = φ
[PROOFSTEP]
apply comp_id
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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) = φ
[PROOFSTEP]
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, ← assoc, hq v.of_succ,
  add_right_eq_self]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
by_cases hqn : n < q
[GOAL]
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.obj (op [n + 1])
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
[PROOFSTEP]
exact v.of_succ.comp_Hσ_eq_zero hqn
[GOAL]
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.obj (op [n + 1])
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
[PROOFSTEP]
obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
have hnaq : n = a + q := by linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
linarith
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
have eq :=
  v ⟨a, by linarith⟩
    (by
      simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
      rfl)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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)
[PROOFSTEP]
rfl
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
simp only [Fin.succ_mk] at eq 
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
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
[PROOFSTEP]
simp only [eq, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
[PROOFSTEP]
intro hφ
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q φ
[PROOFSTEP]
rw [← hφ]
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
[PROOFSTEP]
apply HigherFacesVanish.of_comp
[GOAL]
case mp.v
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (n + 1))
[PROOFSTEP]
apply HigherFacesVanish.of_P
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
[PROOFSTEP]
exact HigherFacesVanish.comp_P_eq_self
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q) n ≫ HomologicalComplex.Hom.f (P q) n = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
rcases n with (_ | n)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (P q) Nat.zero ≫ HomologicalComplex.Hom.f (P q) Nat.zero =
    HomologicalComplex.Hom.f (P q) Nat.zero
[PROOFSTEP]
rw [P_f_0_eq q, comp_id]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n) =
    HomologicalComplex.Hom.f (P q) (Nat.succ n)
[PROOFSTEP]
exact (HigherFacesVanish.of_P q n).comp_P_eq_self
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q ≫ P q = P q
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q ≫ P q) n = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
exact P_f_idem q n
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q q ≫ Q q = Q q
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (Q q ≫ Q q) n = HomologicalComplex.Hom.f (Q q) n
[PROOFSTEP]
exact Q_f_idem q n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P Nat.zero) x✝ =
    (fun X => P Nat.zero) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
dsimp [alternatingFaceMapComplex]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ AlternatingFaceMapComplex.map f ≫ P 0 = P 0 ≫ AlternatingFaceMapComplex.map f
[PROOFSTEP]
simp only [P_zero, id_comp, comp_id]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P (Nat.succ q)) x✝ =
    (fun X => P (Nat.succ q)) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ (alternatingFaceMapComplex C).map f ≫ Hσ q =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
erw [(natTransHσ q).naturality f]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f +
      P q ≫ NatTrans.app (natTransHσ q) x✝¹ ≫ (alternatingFaceMapComplex C).map f =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ HomologicalComplex.Hom.f (Q q) n =
    HomologicalComplex.Hom.f (Q q) n ≫ NatTrans.app f (op [n])
[PROOFSTEP]
simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality, sub_comp, sub_left_inj]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ 𝟙 (Y.obj (op [n])) = 𝟙 (X.obj (op [n])) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n
[PROOFSTEP]
simp only [P_zero]
[GOAL]
case zero
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (𝟙 K[X]) n) = HomologicalComplex.Hom.f (𝟙 K[((whiskering C D).obj G).obj X]) n
[PROOFSTEP]
apply G.map_id
[GOAL]
case succ
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n q : ℕ
hq : G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
⊢ G.map (HomologicalComplex.Hom.f (P (Nat.succ q)) n) = HomologicalComplex.Hom.f (P (Nat.succ q)) n
[PROOFSTEP]
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, Functor.map_add,
  Functor.map_comp, hq, map_Hσ]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (Q q) n) = HomologicalComplex.Hom.f (Q q) n
[PROOFSTEP]
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f, P_add_Q_f]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X.obj (op [n]))) = 𝟙 ((((whiskering C D).obj G).obj X).obj (op [n]))
[PROOFSTEP]
apply G.map_id
