case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (trinomial k m n ↑u ↑v ↑w)
p q : ℤ[X]
hp : IsUnitTrinomial p
⊢ ¬IsUnit p
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (trinomial k m n ↑u ↑v ↑w)
exact fun h =>
  ne_zero_of_lt hmn
    ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans
      (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))