case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (Q Nat.zero) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.zero) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
⊢ HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
induction' q with q hq
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (Q Nat.zero) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.zero) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
simp only [Nat.zero_eq, Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
  Finset.filter_False, Finset.sum_empty]
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
by_cases hqn : q + 1 ≤ n + 1
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)

case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
swap
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
rw [Q_is_eventually_constant (show n + 1 ≤ q by linarith), hq]
case neg.e_s
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ Finset.filter (fun i => ↑i < q) Finset.univ = Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
congr 1
case neg.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < q) Finset.univ ↔
    { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
case neg.e_s
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ Finset.filter (fun i => ↑i < q) Finset.univ = Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
ext ⟨x, hx⟩
case neg.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1
case neg.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < q) Finset.univ ↔
    { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
simp only [Nat.succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and]
no goals
case neg.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1
constructor <;> intro <;> linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : ¬q + 1 ≤ n + 1
⊢ n + 1 ≤ q
linarith
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
cases' Nat.le.dest (Nat.succ_le_succ_iff.mp hqn) with a ha
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
symm
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
conv_rhs => rw [sub_eq_add_neg, add_comm]
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
let q' : Fin (n + 1) := ⟨q, Nat.succ_le_iff.mp hqn⟩
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') +
      ∑ x in Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q',
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ SimplicialObject.σ X (↑Fin.rev x) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp)]
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)

case pos.intro.e_a.e_s
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' = Finset.filter (fun i => ↑i < q) Finset.univ
case pos.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') +
      ∑ x in Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q',
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ SimplicialObject.σ X (↑Fin.rev x) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
congr
no goals
case pos.intro.e_a.e_s
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' = Finset.filter (fun i => ↑i < q) Finset.univ
. ext ⟨i, hi⟩
  simp only [Nat.succ_eq_add_one, Nat.lt_succ_iff_lt_or_eq, Finset.mem_univ,
    forall_true_left, Finset.mem_filter, lt_self_iff_false, or_true, and_self, not_true,
    Finset.mem_erase, ne_eq, Fin.mk.injEq, true_and]
  aesop
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ q' ∈ Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
simp
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
have hnaq' : n = a + q := by linarith
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ { val := a, isLt := (_ : a < Nat.succ n) }) ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) }
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.rev q')) ≫ SimplicialObject.σ X (↑Fin.rev q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
simp only [Fin.val_mk, (HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq',
  q'.rev_eq hnaq', neg_neg]
no goals
case pos.intro.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ { val := a, isLt := (_ : a < Nat.succ n) }) ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) }
rfl
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ n = a + q
linarith
case pos.intro.e_a.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ { val := i, isLt := hi } ∈ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' ↔
    { val := i, isLt := hi } ∈ Finset.filter (fun i => ↑i < q) Finset.univ
case pos.intro.e_a.e_s
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' = Finset.filter (fun i => ↑i < q) Finset.univ
ext ⟨i, hi⟩
case pos.intro.e_a.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ (i < q ∨ i = q) ↔ i < q
case pos.intro.e_a.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ { val := i, isLt := hi } ∈ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' ↔
    { val := i, isLt := hi } ∈ Finset.filter (fun i => ↑i < q) Finset.univ
simp only [Nat.succ_eq_add_one, Nat.lt_succ_iff_lt_or_eq, Finset.mem_univ,
  forall_true_left, Finset.mem_filter, lt_self_iff_false, or_true, and_self, not_true,
  Finset.mem_erase, ne_eq, Fin.mk.injEq, true_and]
no goals
case pos.intro.e_a.e_s.a.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ (i < q ∨ i = q) ↔ i < q
aesop