p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
h : p * mirror p = q * mirror q
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
h : p * mirror p = q * mirror q
⊢ q = p ∨ q = mirror p
let f : ℤ[X] → ℤ[X] := fun p => ⟨Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp⟩
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : f (p * mirror p) = f (q * mirror q)
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
h : p * mirror p = q * mirror q
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
⊢ q = p ∨ q = mirror p
replace h := congr_arg f h
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) = f (q * mirror q)
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : f (p * mirror p) = f (q * mirror q)
⊢ q = p ∨ q = mirror p
replace h := (irreducible_aux1 hkm hmn u v w hp).trans h
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) =
    ↑C ↑v * (↑C ↑u * X ^ (m' + n) + ↑C ↑w * X ^ (n - m' + k + n))
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) = f (q * mirror q)
⊢ q = p ∨ q = mirror p
replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : ↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n) = ↑C ↑u * X ^ (m' + n) + ↑C ↑w * X ^ (n - m' + k + n)
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) =
    ↑C ↑v * (↑C ↑u * X ^ (m' + n) + ↑C ↑w * X ^ (n - m' + k + n))
⊢ q = p ∨ q = mirror p
rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
    ↑u = ↑w ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
      ↑u + ↑w = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : ↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n) = ↑C ↑u * X ^ (m' + n) + ↑C ↑w * X ^ (n - m' + k + n)
⊢ q = p ∨ q = mirror p
rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : m = m' ∧ n - m = n - m' ∨ u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ ↑u + ↑w = 0 ∧ m = n - m + k ∧ m' = n - m' + k
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
    ↑u = ↑w ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
      ↑u + ↑w = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
⊢ q = p ∨ q = mirror p
simp only [add_left_inj, Units.eq_iff] at h
case inl.intro
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n ↑u ↑v ↑w
⊢ q = p ∨ q = mirror p

case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n ↑u ↑v ↑u
h : n - (n - m' + k) + k = m'
⊢ q = p ∨ q = mirror p

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : m = m' ∧ n - m = n - m' ∨ u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ ↑u + ↑w = 0 ∧ m = n - m + k ∧ m' = n - m' + k
⊢ q = p ∨ q = mirror p
rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
no goals
case inl.intro
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n ↑u ↑v ↑w
⊢ q = p ∨ q = mirror p
exact Or.inl (hq.trans hp.symm)
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n ↑u ↑v ↑u
h : n - (n - m' + k) + k = m'
⊢ q = mirror p
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n ↑u ↑v ↑u
h : n - (n - m' + k) + k = m'
⊢ q = p ∨ q = mirror p
refine' Or.inr _
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : trinomial k m' n ↑u ↑v ↑u = mirror p
h : n - (n - m' + k) + k = m'
⊢ q = mirror p
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n ↑u ↑v ↑u
h : n - (n - m' + k) + k = m'
⊢ q = mirror p
rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp
no goals
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : trinomial k m' n ↑u ↑v ↑u = mirror p
h : n - (n - m' + k) + k = m'
⊢ q = mirror p
exact hq.trans hp
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ m = m'
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ q = p ∨ q = mirror p
suffices m = m' by
  rw [this] at hp
  exact Or.inl (hq.trans hp.symm)
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n - m' + k
⊢ m = m'

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ m = m'
rw [tsub_add_eq_add_tsub hmn.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm'✝ : m' = n + k - m'
hm' : 2 * m' = n + k
⊢ m = m'

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n + k - m'
⊢ m' ≤ n + k

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n - m' + k
⊢ m = m'

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n + k - m'
⊢ m' ≤ n + k

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm'✝ : m' = n + k - m'
hm' : 2 * m' = n + k
⊢ m = m'

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n + k - m'
⊢ m' ≤ n + k

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm✝ : m = n + k - m
hm : 2 * m = n + k
hm' : m' = n + k - m'
⊢ m' ≤ n + k

case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
exact hmn'.le.trans (Nat.le_add_right n k)
no goals
case inr.inr.intro.intro
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n + k - m
hm' : m' = n - m' + k
⊢ m ≤ n + k
exact hmn.le.trans (Nat.le_add_right n k)
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m' n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
this : m = m'
⊢ q = p ∨ q = mirror p
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
this : m = m'
⊢ q = p ∨ q = mirror p
rw [this] at hp
no goals
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m' n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
this : m = m'
⊢ q = p ∨ q = mirror p
exact Or.inl (hq.trans hp.symm)