-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem irreducible_aux1 {k m n : ℕ} (hkm : k < m) (hmn : m < n) (u v w : Units ℤ)
    (hp : p = trinomial k m n (u : ℤ) v w) :
    C (v : ℤ) * (C (u : ℤ) * X ^ (m + n) + C (w : ℤ) * X ^ (n - m + k + n)) =
      ⟨Finsupp.filter (· ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp⟩

Proof state:
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
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n))
          (Finsupp.single (k + k) (↑u * ↑w) + Finsupp.single (k + (n - m + k)) (↑u * ↑v) +
                Finsupp.single (k + n) (↑u * ↑u) +
              (Finsupp.single (m + k) (↑v * ↑w) + Finsupp.single (m + (n - m + k)) (↑v * ↑v) +
                Finsupp.single (m + n) (↑v * ↑u)) +
            (Finsupp.single (n + k) (↑w * ↑w) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) +
              Finsupp.single (n + n) (↑w * ↑u))) }

Tactic:
rw [Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add,
  Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add]

Result:
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
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
              Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
            (Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
              Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
          (Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
              Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
            Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u))) }

Proof state:
case h
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
⊢ k + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)

Result:
no goals

Proof state:
case h
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
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
intro h

Result:
case h
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
h : m + k ∈ Set.Ioo (k + n) (n + n)
⊢ False

Proof state:
case h
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
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.1.ne rfl

Result:
no goals

Proof state:
case h
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
⊢ m + n ∈ Set.Ioo (k + n) (n + n)

Tactic:
exact ⟨add_lt_add_right hkm n, add_lt_add_right hmn n⟩

Result:
no goals