-- Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
theorem decomposition_Q (n q : ℕ) :
    ((Q q).f (n + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) =
      ∑ i ∈ Finset.filter (fun i : Fin (n + 1) => (i : ℕ) < q) Finset.univ,
        (P i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ (Fin.rev i)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
⊢ (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

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
n : ℕ
⊢ (Q 0).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < 0) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
⊢ (Q (q + 1)).f (n + 1) =
    ∑ i ∈ Finset.filter (fun i => ↑i < q + 1) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Proof state:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
⊢ (Q (q + 1)).f (n + 1) =
    ∑ i ∈ Finset.filter (fun i => ↑i < q + 1) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

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

Result:
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ (Q (q + 1)).f (n + 1) =
    ∑ i ∈ Finset.filter (fun i => ↑i < q + 1) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Proof state:
case pos.intro.e_a.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ∈ (Finset.filter (fun i => ↑i < q + 1) Finset.univ).erase q' ↔
    ⟨i, hi⟩ ∈ Finset.filter (fun i => ↑i < q) Finset.univ

Tactic:
simp only [q', 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]

Result:
case pos.intro.e_a.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ (i < q ∨ i = q) ↔ i < q

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
⊢ (Q (q + 1)).f (n + 1) =
    ∑ i ∈ Finset.filter (fun i => ↑i < q + 1) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
by_cases hqn : q + 1 ≤ n + 1

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

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

Proof state:
case neg.e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : ¬q + 1 ≤ n + 1
⊢ Finset.filter (fun i => ↑i < q) Finset.univ = Finset.filter (fun i => ↑i < q + 1) Finset.univ

Tactic:
ext ⟨x, hx⟩

Result:
case neg.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ ⟨x, hx⟩ ∈ Finset.filter (fun i => ↑i < q) Finset.univ ↔ ⟨x, hx⟩ ∈ Finset.filter (fun i => ↑i < q + 1) Finset.univ

Proof state:
case pos.intro.e_a.e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (Finset.filter (fun i => ↑i < q + 1) Finset.univ).erase q' = Finset.filter (fun i => ↑i < q) Finset.univ

Tactic:
ext ⟨i, hi⟩

Result:
case pos.intro.e_a.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ∈ (Finset.filter (fun i => ↑i < q + 1) Finset.univ).erase q' ↔
    ⟨i, hi⟩ ∈ Finset.filter (fun i => ↑i < q) Finset.univ

Proof state:
case pos.intro.e_a.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ (i < q ∨ i = q) ↔ i < q

Tactic:
aesop

Result:
no goals

Proof state:
case neg.e_s.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ n = a + q

Tactic:
omega

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (Q 0).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < 0) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
  Finset.filter_False, Finset.sum_empty]

Result:
no goals