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
p q : ℤ[X]
hp : IsUnitTrinomial p
h : ∀ (z : ℂ), ¬(↑(aeval z) p = 0 ∧ ↑(aeval z) (mirror p) = 0)
⊢ Irreducible p
refine' hp.irreducible_of_coprime fun q hq hq' => _
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
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
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]
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
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
intro hq''
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
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
rw [natDegree_pos_iff_degree_pos] at hq''
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
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
rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''
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
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
cases' Complex.exists_root hq'' with z hz
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
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
rw [IsRoot, eval_map, ← aeval_def] at hz
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

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
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
refine' h z ⟨_, _⟩
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
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
rcases hq with ⟨p, rfl⟩
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
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
replace hp := hp.leadingCoeff_isUnit
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
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
rw [leadingCoeff_mul] at hp
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
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
replace hp := isUnit_of_mul_isUnit_left hp
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
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
rw [not_lt, le_zero_iff] at this
no goals
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
rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
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
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
cases' hq with g' hg'
no goals
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
rw [hg', aeval_mul, hz, zero_mul]
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
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
cases' hq' with g' hg'
no goals
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
rw [hg', aeval_mul, hz, zero_mul]