-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
h₅ : m + k ∉ Set.Ioo (k + n) (n + n)
h₆ : k + n ∉ Set.Ioo (k + n) (n + n)
h₇ : k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
h₈ : k + k ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }

Tactic:
rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]

Premises used: Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos