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

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

Result:
no goals

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

Tactic:
have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]

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

Tactic:
simp only [ofFinsupp_single]

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 =
    (monomial (m + n)) (↑v * ↑u) + (monomial (n + (n - m + k))) (↑w * ↑v)

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
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)

Tactic:
refine ⟨?_, add_lt_add_left key n⟩

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
⊢ k + n < n + (n - m + k)

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

Tactic:
exact asymm this 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
⊢ n + n ∉ Set.Ioo (k + n) (n + n)

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

Result:
no goals

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.single (m + n) (↑v * ↑u) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) }

Tactic:
rw [ofFinsupp_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.single (m + n) (↑v * ↑u) } + { toFinsupp := Finsupp.single (n + (n - m + k)) (↑w * ↑v) }

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
⊢ n + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.1.ne (add_comm k n)

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

Tactic:
have := h.1

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)
this : k + n < m + k
⊢ False

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 =
    (monomial (m + n)) (↑v * ↑u) + (monomial (n + (n - m + k))) (↑w * ↑v)

Tactic:
rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]

Result:
no goals

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 :=
        0 + 0 + 0 + (0 + 0 + Finsupp.single (m + n) (↑v * ↑u)) + (0 + Finsupp.single (n + (n - m + k)) (↑w * ↑v) + 0) }

Tactic:
simp only [add_zero, zero_add, ofFinsupp_add, ofFinsupp_single]

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.single (m + n) (↑v * ↑u) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) }