[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ coeff (trinomial k m n u v w) n = w
[PROOFSTEP]
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
  if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ coeff (trinomial k m n u v w) m = v
[PROOFSTEP]
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow, if_neg hkm.ne',
  if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ coeff (trinomial k m n u v w) k = u
[PROOFSTEP]
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow, if_pos rfl,
  if_neg hkm.ne, if_neg (hkm.trans hmn).ne, add_zero, add_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ natDegree (trinomial k m n u v w) = n
[PROOFSTEP]
refine'
  natDegree_eq_of_degree_eq_some
    ((Finset.sup_le fun i h => _).antisymm <| le_degree_of_ne_zero <| by rwa [trinomial_leading_coeff' hkm hmn])
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ coeff (trinomial k m n u v w) n ≠ 0
[PROOFSTEP]
rwa [trinomial_leading_coeff' hkm hmn]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ ↑i ≤ ↑n
[PROOFSTEP]
replace h := support_trinomial' k m n u v w h
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑i ≤ ↑n
[PROOFSTEP]
rw [mem_insert, mem_insert, mem_singleton] at h
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑i ≤ ↑n
[PROOFSTEP]
rcases h with (rfl | rfl | rfl)
[GOAL]
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr (hkm.trans hmn).le
[GOAL]
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr hmn.le
[GOAL]
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i
[PROOFSTEP]
exact le_rfl
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ natTrailingDegree (trinomial k m n u v w) = k
[PROOFSTEP]
refine'
  natTrailingDegree_eq_of_trailingDegree_eq_some
    ((Finset.le_inf fun i h => _).antisymm <|
        le_trailingDegree_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ coeff (trinomial k m n u v w) k ≠ 0
[PROOFSTEP]
rwa [trinomial_trailing_coeff' hkm hmn]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ ↑k ≤ ↑i
[PROOFSTEP]
replace h := support_trinomial' k m n u v w h
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑k ≤ ↑i
[PROOFSTEP]
rw [mem_insert, mem_insert, mem_singleton] at h
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑k ≤ ↑i
[PROOFSTEP]
rcases h with (rfl | rfl | rfl)
[GOAL]
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑i
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i
[PROOFSTEP]
exact WithTop.coe_le_coe.mpr hkm.le
[GOAL]
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i
[PROOFSTEP]
exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ leadingCoeff (trinomial k m n u v w) = w
[PROOFSTEP]
rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ trailingCoeff (trinomial k m n u v w) = u
[PROOFSTEP]
rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ Monic (trinomial k m n u v 1)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
✝ : Nontrivial R
⊢ Monic (trinomial k m n u v 1)
[PROOFSTEP]
exact trinomial_leadingCoeff hkm hmn one_ne_zero
[GOAL]
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ mirror (trinomial k m n u v w) = trinomial k (n - m + k) n w v u
[PROOFSTEP]
rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw, trinomial_def, reflect_add,
  reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow, reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le,
  revAt_le hmn.le, revAt_le le_rfl, add_mul, add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
  Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n), ← add_assoc, ←
  trinomial_def]
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
⊢ ¬IsUnit p
[PROOFSTEP]
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
[GOAL]
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)
[PROOFSTEP]
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)))
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
⊢ card (support p) = 3
[PROOFSTEP]
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ card (support (trinomial k m n ↑u ↑v ↑w)) = 3
[PROOFSTEP]
exact card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
q : ℤ[X]
hp : IsUnitTrinomial 0
⊢ False
[PROOFSTEP]
exact Nat.zero_ne_bit1 1 hp.card_support_eq_three
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
k : ℕ
hk : k ∈ support p
⊢ IsUnit (coeff p k)
[PROOFSTEP]
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
[GOAL]
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✝)
[PROOFSTEP]
have := support_trinomial' k m n (u : ℤ) v w hk
[GOAL]
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✝)
[PROOFSTEP]
rw [mem_insert, mem_insert, mem_singleton] at this
[GOAL]
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✝)
[PROOFSTEP]
rcases this with (rfl | rfl | rfl)
[GOAL]
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)
[PROOFSTEP]
refine' ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩
[GOAL]
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
[PROOFSTEP]
rw [trinomial_trailing_coeff' hkm hmn]
[GOAL]
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✝)
[PROOFSTEP]
refine' ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩
[GOAL]
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✝
[PROOFSTEP]
rw [trinomial_middle_coeff hkm hmn]
[GOAL]
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✝)
[PROOFSTEP]
refine' ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩
[GOAL]
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✝
[PROOFSTEP]
rw [trinomial_leading_coeff' hkm hmn]
[GOAL]
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ card (support p) = 3 ∧ ∀ (k : ℕ), k ∈ support p → IsUnit (coeff p k)
[PROOFSTEP]
refine' ⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => _⟩
[GOAL]
p q : ℤ[X]
hp : card (support p) = 3 ∧ ∀ (k : ℕ), k ∈ support p → IsUnit (coeff p k)
⊢ IsUnitTrinomial p
[PROOFSTEP]
obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1
[GOAL]
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)
[PROOFSTEP]
rw [support_trinomial hkm hmn hx hy hz] at hp
[GOAL]
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)
[PROOFSTEP]
replace hx := hp.2 k (mem_insert_self k { m, n })
[GOAL]
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)
[PROOFSTEP]
replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m { n }))
[GOAL]
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)
[PROOFSTEP]
replace hz := hp.2 n (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n)))
[GOAL]
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)
[PROOFSTEP]
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz
[GOAL]
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)
[PROOFSTEP]
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx
[GOAL]
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)
[PROOFSTEP]
rw [if_neg hkm.ne', if_neg hmn.ne] at hy
[GOAL]
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)
[PROOFSTEP]
rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz
[GOAL]
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)
[PROOFSTEP]
simp_rw [mul_zero, zero_add, add_zero] at hx hy hz
[GOAL]
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)
[PROOFSTEP]
exact ⟨k, m, n, hkm, hmn, hx.unit, hy.unit, hz.unit, rfl⟩
[GOAL]
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ coeff (p * mirror p) ((natDegree (p * mirror p) + natTrailingDegree (p * mirror p)) / 2) = 3
[PROOFSTEP]
rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add, Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]
[GOAL]
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ (sum p fun n x => x ^ 2) = 3
[PROOFSTEP]
refine' ⟨_, fun hp => _⟩
[GOAL]
case refine'_1
p q : ℤ[X]
⊢ IsUnitTrinomial p → (sum p fun n x => x ^ 2) = 3
[PROOFSTEP]
rintro ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (sum (trinomial k m n ↑u ↑v ↑w) fun n x => x ^ 2) = 3
[PROOFSTEP]
rw [sum_def, trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,
  sum_insert (mt mem_insert.mp (not_or_of_not hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
  sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn,
  trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3
[PROOFSTEP]
simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq]
[GOAL]
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
⊢ IsUnitTrinomial p
[PROOFSTEP]
have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
  Int.sq_eq_one_of_sq_le_three ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le)
    (mem_support_iff.mp hk)
[GOAL]
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ IsUnitTrinomial p
[PROOFSTEP]
refine' isUnitTrinomial_iff.mpr ⟨_, fun k hk => isUnit_ofPowEqOne (key k hk) two_ne_zero⟩
[GOAL]
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
[PROOFSTEP]
rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_coe] at hp
[GOAL]
case refine'_2
p q : ℤ[X]
hp : ↑(card (support p)) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
[PROOFSTEP]
exact Nat.cast_injective hp
[GOAL]
p q : ℤ[X]
h : p * mirror p = q * mirror q
⊢ IsUnitTrinomial p ↔ IsUnitTrinomial q
[PROOFSTEP]
rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) =
    { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) (p * mirror p).toFinsupp }
[PROOFSTEP]
have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ n - m + k < n
[PROOFSTEP]
rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) =
    { toFinsupp := Finsupp.filter (Set.Ioo (k + n) (n + n)) (p * mirror p).toFinsupp }
[PROOFSTEP]
rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * (↑C ↑u * X ^ (m + n) + ↑C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        Finsupp.filter (Set.Ioo (k + n) (n + n))
          (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp }
[PROOFSTEP]
simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial, toFinsupp_add,
  toFinsupp_monomial]
  -- Porting note: added next line (less powerful `simp`).
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        Finsupp.filter (Set.Ioo (k + n) (n + n))
          (Finsupp.single (k + k) (↑u * ↑w) + Finsupp.single (k + (n - m + k)) (↑u * ↑v) +
                Finsupp.single (k + n) (↑u * ↑u) +
              (Finsupp.single (m + k) (↑v * ↑w) + Finsupp.single (m + (n - m + k)) (↑v * ↑v) +
                Finsupp.single (m + n) (↑v * ↑u)) +
            (Finsupp.single (n + k) (↑w * ↑w) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) +
              Finsupp.single (n + n) (↑w * ↑u))) }
[PROOFSTEP]
rw [Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add,
  Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
            (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
          (Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
              Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
            Finsupp.filter (Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u))) }
[PROOFSTEP]
rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
  Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
  Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        0 + 0 + 0 + (0 + 0 + Finsupp.single (m + n) (↑v * ↑u)) + (0 + Finsupp.single (n + (n - m + k)) (↑w * ↑v) + 0) }
[PROOFSTEP]
simp only [add_zero, zero_add, ofFinsupp_add, ofFinsupp_single]
  -- Porting note: added next two lines (less powerful `simp`).
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    { toFinsupp := Finsupp.single (m + n) (↑v * ↑u) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) }
[PROOFSTEP]
rw [ofFinsupp_add]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    { toFinsupp := Finsupp.single (m + n) (↑v * ↑u) } + { toFinsupp := Finsupp.single (n + (n - m + k)) (↑w * ↑v) }
[PROOFSTEP]
simp only [ofFinsupp_single]
[GOAL]
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ↑C ↑v * ↑(monomial (m + n)) ↑u + ↑C ↑v * ↑(monomial (n - m + k + n)) ↑w =
    ↑(monomial (m + n)) (↑v * ↑u) + ↑(monomial (n + (n - m + k))) (↑w * ↑v)
[PROOFSTEP]
rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (n + n)
[PROOFSTEP]
exact fun h => h.2.ne rfl
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ Set.Ioo (k + n) (n + n) (n + (n - m + k))
[PROOFSTEP]
refine' ⟨_, add_lt_add_left key n⟩
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n < n + (n - m + k)
[PROOFSTEP]
rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (n + k)
[PROOFSTEP]
exact fun h => h.1.ne (add_comm k n)
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ Set.Ioo (k + n) (n + n) (m + n)
[PROOFSTEP]
exact ⟨add_lt_add_right hkm n, add_lt_add_right hmn n⟩
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (m + (n - m + k))
[PROOFSTEP]
rw [← add_assoc, add_tsub_cancel_of_le hmn.le, add_comm]
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (n + k) (n + n) (n + k)
[PROOFSTEP]
exact fun h => h.1.ne rfl
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (m + k)
[PROOFSTEP]
intro h
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
h : Set.Ioo (k + n) (n + n) (m + k)
⊢ False
[PROOFSTEP]
have := h.1
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
h : Set.Ioo (k + n) (n + n) (m + k)
this : k + n < m + k
⊢ False
[PROOFSTEP]
rw [add_comm, add_lt_add_iff_right] at this
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
h : Set.Ioo (k + n) (n + n) (m + k)
this : n < m
⊢ False
[PROOFSTEP]
exact asymm this hmn
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (k + n)
[PROOFSTEP]
exact fun h => h.1.ne rfl
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (k + (n - m + k))
[PROOFSTEP]
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) key
[GOAL]
case h
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ ¬Set.Ioo (k + n) (n + n) (k + k)
[PROOFSTEP]
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)
[GOAL]
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
[PROOFSTEP]
let f : ℤ[X] → ℤ[X] := fun p => ⟨Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp⟩
[GOAL]
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
[PROOFSTEP]
replace h := congr_arg f h
[GOAL]
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
[PROOFSTEP]
replace h := (irreducible_aux1 hkm hmn u v w hp).trans h
[GOAL]
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
[PROOFSTEP]
replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm
[GOAL]
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
[PROOFSTEP]
rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h
[GOAL]
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
[PROOFSTEP]
rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h
[GOAL]
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
[PROOFSTEP]
simp only [add_left_inj, Units.eq_iff] at h
[GOAL]
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
[PROOFSTEP]
rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
[GOAL]
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
[PROOFSTEP]
exact Or.inl (hq.trans hp.symm)
[GOAL]
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
[PROOFSTEP]
refine' Or.inr _
[GOAL]
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
[PROOFSTEP]
rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp
[GOAL]
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
[PROOFSTEP]
exact hq.trans hp
[GOAL]
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
[PROOFSTEP]
suffices m = m' by
  rw [this] at hp
  exact Or.inl (hq.trans hp.symm)
[GOAL]
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
[PROOFSTEP]
rw [this] at hp
[GOAL]
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
[PROOFSTEP]
exact Or.inl (hq.trans hp.symm)
[GOAL]
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'
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hmn.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm
[GOAL]
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
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
[GOAL]
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
[PROOFSTEP]
exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
[GOAL]
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
[PROOFSTEP]
exact hmn'.le.trans (Nat.le_add_right n k)
[GOAL]
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
[PROOFSTEP]
exact hmn.le.trans (Nat.le_add_right n k)
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
have hmul := congr_arg leadingCoeff h
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : leadingCoeff (p * mirror p) = leadingCoeff (q * mirror q)
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [leadingCoeff_mul, leadingCoeff_mul, mirror_leadingCoeff, mirror_leadingCoeff, hp, hq,
  trinomial_leadingCoeff hkm hmn w.ne_zero, trinomial_leadingCoeff hkm' hmn' z.ne_zero,
  trinomial_trailingCoeff hkm hmn u.ne_zero, trinomial_trailingCoeff hkm' hmn' x.ne_zero] at hmul
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
have hadd := congr_arg (eval 1) h
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 (p * mirror p) = eval 1 (q * mirror q)
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [eval_mul, eval_mul, mirror_eval_one, mirror_eval_one, ← sq, ← sq, hp, hq] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 (trinomial k m n ↑u ↑v ↑w) ^ 2 = eval 1 (trinomial k m' n ↑x ↑v ↑z) ^ 2
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
simp only [eval_add, eval_C_mul, eval_pow, eval_X, one_pow, mul_one, trinomial_def] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑u + ↑v + ↑w) ^ 2 = (↑x + ↑v + ↑z) ^ 2
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [add_assoc, add_assoc, add_comm (u : ℤ), add_comm (x : ℤ), add_assoc, add_assoc] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑v + (↑w + ↑u)) ^ 2 = (↑v + (↑z + ↑x)) ^ 2
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
simp only [add_sq', add_assoc, add_right_inj, ← Units.val_pow_eq_pow_val, Int.units_sq] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * ↑w * ↑u + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [mul_assoc, hmul, ← mul_assoc, add_right_inj,
  mul_right_inj' (show 2 * (v : ℤ) ≠ 0 from mul_ne_zero two_ne_zero v.ne_zero)] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : ↑w + ↑u = ↑z + ↑x
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
replace hadd := (Int.isUnit_add_isUnit_eq_isUnit_add_isUnit w.isUnit u.isUnit z.isUnit x.isUnit).mp hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : ↑w = ↑z ∧ ↑u = ↑x ∨ ↑w = ↑x ∧ ↑u = ↑z
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
simp only [Units.eq_iff] at hadd
[GOAL]
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * mirror p = q * mirror q
hmul : ↑w * ↑u = ↑z * ↑x
hadd : w = z ∧ u = x ∨ w = x ∧ u = z
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rcases hadd with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case inl.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
h : p * mirror p = q * mirror q
hq : q = trinomial k m' n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑w * ↑u
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
exact irreducible_aux2 hkm hmn hkm' hmn' u v w hp hq h
[GOAL]
case inr.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
h : p * mirror p = q * mirror q
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [← mirror_inj, trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero] at hq
[GOAL]
case inr.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
h : p * mirror p = q * mirror q
hq : mirror q = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [mul_comm q, ← q.mirror_mirror, q.mirror.mirror_mirror] at h
[GOAL]
case inr.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
h : p * mirror p = mirror q * mirror (mirror q)
hq : mirror q = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = mirror p
[PROOFSTEP]
rw [← mirror_inj, or_comm, ← mirror_eq_iff]
[GOAL]
case inr.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
h : p * mirror p = mirror q * mirror (mirror q)
hq : mirror q = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ mirror q = p ∨ mirror q = mirror p
[PROOFSTEP]
exact
  irreducible_aux2 hkm hmn (lt_add_of_pos_left k (tsub_pos_of_lt hmn'))
    (lt_tsub_iff_right.mp ((tsub_lt_tsub_iff_left_of_le hmn'.le).mpr hkm')) u v w hp hq h
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
⊢ Irreducible p
[PROOFSTEP]
refine' irreducible_of_mirror hp.not_isUnit (fun q hpq => _) h
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
have hq : IsUnitTrinomial q := (isUnitTrinomial_iff'' hpq).mp hp
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
hq : IsUnitTrinomial q
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
hq : IsUnitTrinomial q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
obtain ⟨k', m', n', hkm', hmn', x, y, z, hq⟩ := hq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
have hk : k = k' := by
  rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ←
    natTrailingDegree_mul_mirror, hpq, natTrailingDegree_mul_mirror, hq,
    trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
[GOAL]
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ k = k'
[PROOFSTEP]
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ←
  natTrailingDegree_mul_mirror, hpq, natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
have hn : n = n' := by
  rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ← hp, ←
    natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq, trinomial_natDegree hkm' hmn' z.ne_zero]
[GOAL]
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ n = n'
[PROOFSTEP]
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ← hp, ←
  natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq, trinomial_natDegree hkm' hmn' z.ne_zero]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
hn : n = n'
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
subst hk
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
subst hn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ) ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
  (h1 | h1)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = ↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rw [h1] at hq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = p
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
exact Or.inl h2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = mirror p
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
exact Or.inr (Or.inr (Or.inl h2))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rw [h1] at hq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rw [trinomial_def] at hp
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = ↑C ↑u * X ^ k + ↑C ↑v * X ^ m + ↑C ↑w * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg] at hp
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq : p * mirror p = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp✝ : p = ↑C ↑u * X ^ k + ↑C ↑v * X ^ m + ↑C ↑w * X ^ n
hp : -p = ↑C (-↑u) * X ^ k + ↑C (-↑v) * X ^ m + ↑C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rw [← neg_mul_neg, ← mirror_neg] at hpq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
p q✝ : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
q : ℤ[X]
hpq✝ : p * mirror p = q * mirror q
hpq : -p * mirror (-p) = q * mirror q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp✝ : p = ↑C ↑u * X ^ k + ↑C ↑v * X ^ m + ↑C ↑w * X ^ n
hp : -p = ↑C (-↑u) * X ^ k + ↑C (-↑v) * X ^ m + ↑C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = mirror p ∨ q = -mirror p
[PROOFSTEP]
rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.inl
p q : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp✝ : p = ↑C ↑u * X ^ k + ↑C ↑v * X ^ m + ↑C ↑w * X ^ n
hp : -p = ↑C (-↑u) * X ^ k + ↑C (-↑v) * X ^ m + ↑C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq✝ : p * mirror p = -p * mirror (-p)
hpq : -p * mirror (-p) = -p * mirror (-p)
hq : -p = trinomial k m' n (↑x) (-↑v) ↑z
⊢ -p = p ∨ -p = -p ∨ -p = mirror p ∨ -p = -mirror p
[PROOFSTEP]
exact Or.inr (Or.inl rfl)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
p q : ℤ[X]
h : ∀ (q : ℤ[X]), q ∣ p → q ∣ mirror p → IsUnit q
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp✝ : p = ↑C ↑u * X ^ k + ↑C ↑v * X ^ m + ↑C ↑w * X ^ n
hp : -p = ↑C (-↑u) * X ^ k + ↑C (-↑v) * X ^ m + ↑C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq✝ : p * mirror p = mirror (-p) * mirror (mirror (-p))
hpq : -p * mirror (-p) = mirror (-p) * mirror (mirror (-p))
hq : mirror (-p) = trinomial k m' n (↑x) (-↑v) ↑z
⊢ mirror (-p) = p ∨ mirror (-p) = -p ∨ mirror (-p) = mirror p ∨ mirror (-p) = -mirror p
[PROOFSTEP]
exact Or.inr (Or.inr (Or.inr p.mirror_neg))
[GOAL]
p q : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
⊢ Irreducible p
[PROOFSTEP]
refine' hp.irreducible_of_coprime fun q hq hq' => _
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
⊢ IsUnit q
[PROOFSTEP]
suffices ¬0 < q.natDegree by
  rcases hq with ⟨p, rfl⟩
  replace hp := hp.leadingCoeff_isUnit
  rw [leadingCoeff_mul] at hp
  replace hp := isUnit_of_mul_isUnit_left hp
  rw [not_lt, le_zero_iff] at this
  rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
this : ¬0 < natDegree q
⊢ IsUnit q
[PROOFSTEP]
rcases hq with ⟨p, rfl⟩
[GOAL]
case intro
q✝ q : ℤ[X]
this : ¬0 < natDegree q
p : ℤ[X]
hp : IsUnitTrinomial (q * p)
h : ∀ (z : ℂ), ¬(↑(aeval z) (q * p) = 0 ∧ ↑(aeval z) (mirror (q * p)) = 0)
hq' : q ∣ mirror (q * p)
⊢ IsUnit q
[PROOFSTEP]
replace hp := hp.leadingCoeff_isUnit
[GOAL]
case intro
q✝ q : ℤ[X]
this : ¬0 < natDegree q
p : ℤ[X]
h : ∀ (z : ℂ), ¬(↑(aeval z) (q * p) = 0 ∧ ↑(aeval z) (mirror (q * p)) = 0)
hq' : q ∣ mirror (q * p)
hp : IsUnit (leadingCoeff (q * p))
⊢ IsUnit q
[PROOFSTEP]
rw [leadingCoeff_mul] at hp
[GOAL]
case intro
q✝ q : ℤ[X]
this : ¬0 < natDegree q
p : ℤ[X]
h : ∀ (z : ℂ), ¬(↑(aeval z) (q * p) = 0 ∧ ↑(aeval z) (mirror (q * p)) = 0)
hq' : q ∣ mirror (q * p)
hp : IsUnit (leadingCoeff q * leadingCoeff p)
⊢ IsUnit q
[PROOFSTEP]
replace hp := isUnit_of_mul_isUnit_left hp
[GOAL]
case intro
q✝ q : ℤ[X]
this : ¬0 < natDegree q
p : ℤ[X]
h : ∀ (z : ℂ), ¬(↑(aeval z) (q * p) = 0 ∧ ↑(aeval z) (mirror (q * p)) = 0)
hq' : q ∣ mirror (q * p)
hp : IsUnit (leadingCoeff q)
⊢ IsUnit q
[PROOFSTEP]
rw [not_lt, le_zero_iff] at this
[GOAL]
case intro
q✝ q : ℤ[X]
this : natDegree q = 0
p : ℤ[X]
h : ∀ (z : ℂ), ¬(↑(aeval z) (q * p) = 0 ∧ ↑(aeval z) (mirror (q * p)) = 0)
hq' : q ∣ mirror (q * p)
hp : IsUnit (leadingCoeff q)
⊢ IsUnit q
[PROOFSTEP]
rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
⊢ ¬0 < natDegree q
[PROOFSTEP]
intro hq''
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < natDegree q
⊢ False
[PROOFSTEP]
rw [natDegree_pos_iff_degree_pos] at hq''
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree q
⊢ False
[PROOFSTEP]
rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''
[GOAL]
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
⊢ False
[PROOFSTEP]
cases' Complex.exists_root hq'' with z hz
[GOAL]
case intro
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : IsRoot (map (algebraMap ℤ ℂ) q) z
⊢ False
[PROOFSTEP]
rw [IsRoot, eval_map, ← aeval_def] at hz
[GOAL]
case intro
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : ↑(aeval z) q = 0
⊢ False
[PROOFSTEP]
refine' h z ⟨_, _⟩
[GOAL]
case intro.refine'_1
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : ↑(aeval z) q = 0
⊢ ↑(aeval z) p = 0
[PROOFSTEP]
cases' hq with g' hg'
[GOAL]
case intro.refine'_1.intro
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : ↑(aeval z) q = 0
g' : ℤ[X]
hg' : p = q * g'
⊢ ↑(aeval z) p = 0
[PROOFSTEP]
rw [hg', aeval_mul, hz, zero_mul]
[GOAL]
case intro.refine'_2
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ mirror p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : ↑(aeval z) q = 0
⊢ ↑(aeval z) (mirror p) = 0
[PROOFSTEP]
cases' hq' with g' hg'
[GOAL]
case intro.refine'_2.intro
p q✝ : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < degree (map (algebraMap ℤ ℂ) q)
z : ℂ
hz : ↑(aeval z) q = 0
g' : ℤ[X]
hg' : mirror p = q * g'
⊢ ↑(aeval z) (mirror p) = 0
[PROOFSTEP]
rw [hg', aeval_mul, hz, zero_mul]


[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∈ f.support ↔ (fun i => {↑f i}) i ≠ 0
[PROOFSTEP]
rw [← not_iff_not, not_mem_support_iff, not_ne_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ ↑f i = 0 ↔ (fun i => {↑f i}) i = 0
[PROOFSTEP]
exact singleton_injective.eq_iff.symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∈ f.support ∪ g.support ↔ (fun i => Icc (↑f i) (↑g i)) i ≠ 0
[PROOFSTEP]
rw [mem_union, ← not_iff_not, not_or, not_mem_support_iff, not_mem_support_iff, not_ne_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ ↑f i = 0 ∧ ↑g i = 0 ↔ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
exact Icc_eq_singleton_iff.symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ x ∈ (fun f g => Finset.finsupp (f.support ∪ g.support) ↑(rangeIcc f g)) f g ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
refine' (mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), ↑x i ∈ ↑(rangeIcc f g) i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
simp_rw [mem_rangeIcc_apply_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), ↑f i ≤ ↑x i ∧ ↑x i ≤ ↑g i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
exact forall_and
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Icc f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i))
[PROOFSTEP]
simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ico f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ioc f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ioo f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (uIcc f g) = ∏ i in f.support ∪ g.support, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
rw [← support_inf_union_support_sup]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (uIcc f g) = ∏ i in (f ⊓ g).support ∪ (f ⊔ g).support, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
exact card_Icc (_ : ι →₀ α) _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
[PROOFSTEP]
classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iio f) = ∏ i in f.support, card (Iic (↑f i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]


[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
inst✝ : LE α
f g : ι →₀ α
h : (fun f => ↑f) f = (fun f => ↑f) g
i : ι
⊢ ↑f i = ↑g i
[PROOFSTEP]
dsimp at h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
inst✝ : LE α
f g : ι →₀ α
h : ↑f = ↑g
i : ι
⊢ ↑f i = ↑g i
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
[PROOFSTEP]
simp [inf_eq_and_sup_eq_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
⊢ ∀ (a : ι →₀ α), ⊥ ≤ a
[PROOFSTEP]
simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
⊢ f + g = 0 ↔ f = 0 ∧ g = 0
[PROOFSTEP]
simp [FunLike.ext_iff, forall_and]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ (i : ι), i ∈ s✝ → ↑f i ≤ ↑g i
s : ι
⊢ ↑f s ≤ ↑g s
[PROOFSTEP]
classical exact if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ (i : ι), i ∈ s✝ → ↑f i ≤ ↑g i
s : ι
⊢ ↑f s ≤ ↑g s
[PROOFSTEP]
exact if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
i : ι
x : α
f : ι →₀ α
⊢ (∀ (i_1 : ι), i_1 ∈ {i} → ↑(single i x) i_1 ≤ ↑f i_1) ↔ x ≤ ↑f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ single i (a - b) = single i a - single i b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
obtain rfl | h := eq_or_ne i j
[GOAL]
case h.inl
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i
[PROOFSTEP]
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
[GOAL]
case h.inr
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support
[PROOFSTEP]
simp (config := { contextual := true }) only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, Ne.def, coe_tsub,
  Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
inst✝ : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support
[PROOFSTEP]
simp (config := { contextual := true }) [subset_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
[PROOFSTEP]
simp only [inf_apply, mem_support_iff, Ne.def, Finset.mem_union, Finset.mem_filter, Finset.mem_inter]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊓ ↑g a✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
[PROOFSTEP]
simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
[PROOFSTEP]
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne.def, ← bot_eq_zero]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
[PROOFSTEP]
rw [_root_.sup_eq_bot_iff, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
[PROOFSTEP]
classical
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty, Finsupp.support_inf]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
[PROOFSTEP]
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty, Finsupp.support_inf]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
⊢ List α ≃ DList α
[PROOFSTEP]
refine'
  { toFun := DList.ofList
    invFun := DList.toList .. }
[GOAL]
case refine'_1
α : Type u_1
⊢ LeftInverse toList ofList
[PROOFSTEP]
simp [Function.RightInverse, Function.LeftInverse, DList.toList_ofList, DList.ofList_toList]
[GOAL]
case refine'_2
α : Type u_1
⊢ Function.RightInverse toList ofList
[PROOFSTEP]
simp [Function.RightInverse, Function.LeftInverse, DList.toList_ofList, DList.ofList_toList]


[GOAL]
m n : ℕ∞
⊢ ↑(↑toNat ⊤) = ⊤ ↔ ⊤ ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
m n : ℕ∞
x✝ : ℕ
⊢ ↑(↑toNat ↑x✝) = ↑x✝ ↔ ↑x✝ ≠ ⊤
[PROOFSTEP]
simp [toNat_coe]
[GOAL]
m✝ n✝ m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ ↑toNat (m + n) = ↑toNat m + ↑toNat n
[PROOFSTEP]
lift m to ℕ using hm
[GOAL]
case intro
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ ↑toNat (↑m + n) = ↑toNat ↑m + ↑toNat n
[PROOFSTEP]
lift n to ℕ using hn
[GOAL]
case intro.intro
m✝ n✝ : ℕ∞
m n : ℕ
⊢ ↑toNat (↑m + ↑n) = ↑toNat ↑m + ↑toNat ↑n
[PROOFSTEP]
rfl
[GOAL]
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ ↑toNat (m - n) = ↑toNat m - ↑toNat n
[PROOFSTEP]
lift n to ℕ using hn
[GOAL]
case intro
m✝ n✝ m : ℕ∞
n : ℕ
⊢ ↑toNat (m - ↑n) = ↑toNat m - ↑toNat ↑n
[PROOFSTEP]
induction m using ENat.recTopCoe
[GOAL]
case intro.h₁
m n✝ : ℕ∞
n : ℕ
⊢ ↑toNat (⊤ - ↑n) = ↑toNat ⊤ - ↑toNat ↑n
[PROOFSTEP]
rw [top_sub_coe, toNat_top, zero_tsub]
[GOAL]
case intro.h₂
m n✝ : ℕ∞
n a✝ : ℕ
⊢ ↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
[PROOFSTEP]
rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
[GOAL]
m✝ n✝ m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ ↑toNat m = n ↔ m = ↑n
[PROOFSTEP]
induction m using ENat.recTopCoe
[GOAL]
case h₁
m n✝ : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ ↑toNat ⊤ = n ↔ ⊤ = ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
case h₂
m n✝ : ℕ∞
n : ℕ
hn : n ≠ 0
a✝ : ℕ
⊢ ↑toNat ↑a✝ = n ↔ ↑a✝ = ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
m✝ n m : ℕ∞
⊢ Order.succ m = m + 1
[PROOFSTEP]
cases m
[GOAL]
case none
m n : ℕ∞
⊢ Order.succ none = none + 1
[PROOFSTEP]
rfl
[GOAL]
case some
m n : ℕ∞
val✝ : ℕ
⊢ Order.succ (some val✝) = some val✝ + 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ∞
hm : m ≠ ⊤
⊢ ¬IsMax m
[PROOFSTEP]
rwa [isMax_iff_eq_top]
[GOAL]
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
⊢ P a
[PROOFSTEP]
have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc
[GOAL]
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a
[PROOFSTEP]
cases a
[GOAL]
case none
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P none
[PROOFSTEP]
exact htop A
[GOAL]
case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
[PROOFSTEP]
exact A _