-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem coeff_isUnit (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) :
    IsUnit (p.coeff k)

Proof state:
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ ↑u = (trinomial k m n ↑u ↑v ↑w).coeff k

Tactic:
rw [trinomial_trailing_coeff' hkm hmn]

Result:
no goals

Proof state:
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ ↑v = (trinomial k k✝ n ↑u ↑v ↑w).coeff k✝

Tactic:
rw [trinomial_middle_coeff hkm hmn]

Result:
no goals

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

Tactic:
refine ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
have := support_trinomial' k m n (u : ℤ) v w hk

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ ∈ {k, m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Tactic:
refine ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ ∈ {k, m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at this

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ = m ∨ k✝ = n
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k)

Tactic:
refine ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩

Result:
no goals

Proof state:
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ ↑w = (trinomial k m k✝ ↑u ↑v ↑w).coeff k✝

Tactic:
rw [trinomial_leading_coeff' hkm hmn]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ = m ∨ k✝ = n
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
rcases this with (rfl | rfl | rfl)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k)

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

case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Proof state:
p : ℤ[X]
hp : p.IsUnitTrinomial
k : ℕ
hk : k ∈ p.support
⊢ IsUnit (p.coeff k)

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)