case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
p q : ℤ[X]
hp : IsUnitTrinomial p
k : ℕ
hk : k ∈ support p
⊢ IsUnit (coeff p k)
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
this : k✝ ∈ {k, m, n}
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
have := support_trinomial' k m n (u : ℤ) v w hk
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
this : k✝ = k ∨ k✝ = m ∨ k✝ = n
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
this : k✝ ∈ {k, m, n}
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
rw [mem_insert, mem_insert, mem_singleton] at this
case intro.intro.intro.intro.intro.intro.intro.intro.inl
q : ℤ[X]
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k)

case intro.intro.intro.intro.intro.intro.intro.intro.inr.inl
q : ℤ[X]
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ support (trinomial k k✝ n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k k✝ n ↑u ↑v ↑w) k✝)

case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
q : ℤ[X]
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ support (trinomial k m k✝ ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m k✝ ↑u ↑v ↑w) k✝)
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ support (trinomial k m n ↑u ↑v ↑w)
this : k✝ = k ∨ k✝ = m ∨ k✝ = n
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k✝)
rcases this with (rfl | rfl | rfl)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inl
q : ℤ[X]
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m n ↑u ↑v ↑w) k)
refine' ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩
no goals
q : ℤ[X]
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n ↑u ↑v ↑w)
⊢ ↑u = coeff (trinomial k m n ↑u ↑v ↑w) k
rw [trinomial_trailing_coeff' hkm hmn]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr.inl
q : ℤ[X]
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ support (trinomial k k✝ n ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k k✝ n ↑u ↑v ↑w) k✝)
refine' ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩
no goals
q : ℤ[X]
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ support (trinomial k k✝ n ↑u ↑v ↑w)
⊢ ↑v = coeff (trinomial k k✝ n ↑u ↑v ↑w) k✝
rw [trinomial_middle_coeff hkm hmn]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
q : ℤ[X]
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ support (trinomial k m k✝ ↑u ↑v ↑w)
⊢ IsUnit (coeff (trinomial k m k✝ ↑u ↑v ↑w) k✝)
refine' ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩
no goals
q : ℤ[X]
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ support (trinomial k m k✝ ↑u ↑v ↑w)
⊢ ↑w = coeff (trinomial k m k✝ ↑u ↑v ↑w) k✝
rw [trinomial_leading_coeff' hkm hmn]