p q : ℤ[X]
hp : card (support p) = 3 ∧ ∀ (k : ℕ), k ∈ support p → IsUnit (coeff p k)
⊢ IsUnitTrinomial p
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ card (support p) = 3 ∧ ∀ (k : ℕ), k ∈ support p → IsUnit (coeff p k)
refine' ⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3 ∧
    ∀ (k_1 : ℕ),
      k_1 ∈ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) →
        IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
p q : ℤ[X]
hp : card (support p) = 3 ∧ ∀ (k : ℕ), k ∈ support p → IsUnit (coeff p k)
⊢ IsUnitTrinomial p
obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3 ∧
    ∀ (k_1 : ℕ),
      k_1 ∈ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) →
        IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
rw [support_trinomial hkm hmn hx hy hz] at hp
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
replace hx := hp.2 k (mem_insert_self k {m, n})
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
hy : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) m)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m {n}))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
hy : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) m)
hz : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) n)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hz : z ≠ 0
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
hy : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) m)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
replace hz := hp.2 n (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n)))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k)
hy : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) m)
hz : IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) n)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
rw [if_neg hkm.ne', if_neg hmn.ne] at hy
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hz : IsUnit z
hx : IsUnit x
hy : IsUnit y
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
simp_rw [MulZeroClass.mul_zero, zero_add, add_zero] at hx hy hz
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : card {k, m, n} = 3 ∧ ∀ (k_1 : ℕ), k_1 ∈ {k, m, n} → IsUnit (coeff (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) k_1)
hz : IsUnit z
hx : IsUnit x
hy : IsUnit y
⊢ IsUnitTrinomial (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
exact ⟨k, m, n, hkm, hmn, hx.unit, hy.unit, hz.unit, rfl⟩