-- 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:
case pos.intro.e_a
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, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

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

Result:
case pos.intro.e_a
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, ⋯⟩
hnaq' : n = a + q
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

Proof state:
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

Tactic:
rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]

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

Tactic:
simp [q']

Result:
no goals

Proof state:
case pos.intro.e_a
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, ⋯⟩
hnaq' : n = a + q
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

Tactic:
simp only [Fin.val_mk, (HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq',
  q'.rev_eq hnaq', neg_neg]

Result:
case pos.intro.e_a
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, ⋯⟩
hnaq' : n = a + q
⊢ (P ↑q').f (n + 1) ≫ X.δ ⟨a, ⋯⟩.succ ≫ X.σ ⟨a, ⋯⟩ = (P q).f (n + 1) ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

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

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

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

Tactic:
congr 1

Result:
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

Proof state:
case pos.intro.e_a
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, ⋯⟩
hnaq' : n = a + q
⊢ (P ↑q').f (n + 1) ≫ X.δ ⟨a, ⋯⟩.succ ≫ X.σ ⟨a, ⋯⟩ = (P q).f (n + 1) ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
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' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev +
      ∑ x ∈ (Finset.filter (fun i => ↑i < q + 1) Finset.univ).erase q', (P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev =
    -(P q).f (n + 1) ≫ (Hσ 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:
congr

Result:
case pos.intro.e_a
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, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

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