x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
rid : ¬1 < natDegree p
⊢ False
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
⊢ 1 < natDegree p
by_contra rid
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
rid : ¬1 < natDegree (↑C a * X + ↑C b)
⊢ False
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
rid : ¬1 < natDegree p
⊢ False
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ False
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
rid : ¬1 < natDegree (↑C a * X + ↑C b)
⊢ False
clear rid
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
⊢ False
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ False
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
case intro.intro.inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ False

case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
⊢ False
rcases em (a = 0) with (rfl | ha)
no goals
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ ↑a * x = -↑b
simpa [eq_neg_iff_add_eq_zero] using x_is_root
case intro.intro.inl
x : ℝ
hx : Irrational x
p_nonzero : ↑C 0 * X + ↑C 0 ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C 0) = 0
this : ↑0 * x = -↑0
⊢ False
case intro.intro.inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ False
obtain rfl : b = 0 := by simpa
no goals
case intro.intro.inl
x : ℝ
hx : Irrational x
p_nonzero : ↑C 0 * X + ↑C 0 ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C 0) = 0
this : ↑0 * x = -↑0
⊢ False
simp at p_nonzero
no goals
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ b = 0
simpa
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ ↑(-↑b / ↑a) = x

case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
refine' hx ⟨-b / a, _⟩
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ ↑(-↑b / ↑a) = x

case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
assumption_mod_cast
no goals
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
assumption_mod_cast