p q : ℤ[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 (Set.Ioo (k + n) (n + n)) (p * mirror p).toFinsupp }
p q : ℤ[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 (Set.Ioo (k + n) (n + n)) (p * mirror p).toFinsupp }
have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
p q : ℤ[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 (Set.Ioo (k + n) (n + n))
          (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp }
p q : ℤ[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 (Set.Ioo (k + n) (n + n)) (p * mirror p).toFinsupp }
rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]
p q : ℤ[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 (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))) }
p q : ℤ[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 (Set.Ioo (k + n) (n + n))
          (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp }
simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial,
  toFinsupp_add, toFinsupp_monomial, Finsupp.filter_add]
p q : ℤ[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 (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
            (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
          (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
            Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u))) }
p q : ℤ[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 (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))) }
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]
p q : ℤ[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) }

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (n + n)

case h
p q : ℤ[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
⊢ Set.Ioo (k + n) (n + n) (n + (n - m + k))

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (n + k)

case h
p q : ℤ[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
⊢ Set.Ioo (k + n) (n + n) (m + n)

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (m + (n - m + k))

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (m + k)

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + n)

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + (n - m + k))

case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + k)
p q : ℤ[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 (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
            (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
          (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
            Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u))) }
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]
no goals
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ n - m + k < n
rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
p q : ℤ[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) }
p q : ℤ[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) }
simp only [add_zero, zero_add, ofFinsupp_add, ofFinsupp_single]
p q : ℤ[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) }
p q : ℤ[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) }
rw [ofFinsupp_add]
p q : ℤ[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)
p q : ℤ[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) }
simp only [ofFinsupp_single]
no goals
p q : ℤ[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)
rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (n + n)
exact fun h => h.2.ne rfl
case h
p q : ℤ[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)
case h
p q : ℤ[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
⊢ Set.Ioo (k + n) (n + n) (n + (n - m + k))
refine' ⟨_, add_lt_add_left key n⟩
no goals
case h
p q : ℤ[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)
rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (n + k)
exact fun h => h.1.ne (add_comm k n)
no goals
case h
p q : ℤ[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
⊢ Set.Ioo (k + n) (n + n) (m + n)
exact ⟨add_lt_add_right hkm n, add_lt_add_right hmn n⟩
case h
p q : ℤ[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
⊢ ¬Set.Ioo (n + k) (n + n) (n + k)
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (m + (n - m + k))
rw [← add_assoc, add_tsub_cancel_of_le hmn.le, add_comm]
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (n + k) (n + n) (n + k)
exact fun h => h.1.ne rfl
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
⊢ False
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (m + k)
intro h
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
this : k + n < m + k
⊢ False
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
⊢ False
have := h.1
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
this : n < m
⊢ False
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
this : k + n < m + k
⊢ False
rw [add_comm, add_lt_add_iff_right] at this
no goals
case h
p q : ℤ[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 : Set.Ioo (k + n) (n + n) (m + k)
this : n < m
⊢ False
exact asymm this hmn
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + n)
exact fun h => h.1.ne rfl
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + (n - m + k))
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) key
no goals
case h
p q : ℤ[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
⊢ ¬Set.Ioo (k + n) (n + n) (k + k)
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)