-- Mathlib/Data/Real/Irrational.lean
theorem one_lt_natDegree_of_irrational_root (hx : Irrational x) (p_nonzero : p ≠ 0)
    (x_is_root : aeval x p = 0) : 1 < p.natDegree

Proof state:
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

Tactic:
simpa [eq_neg_iff_add_eq_zero] using x_is_root

Result:
no goals

Proof state:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
rid : ¬1 < p.natDegree
⊢ False

Tactic:
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩

Result:
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 < (C a * X + C b).natDegree
⊢ False

Proof state:
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

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
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

Tactic:
refine hx ⟨-b / a, ?_⟩

Result:
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

Proof state:
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

Tactic:
simp at p_nonzero

Result:
no goals

Proof state:
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

Tactic:
rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this

Result:
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

Proof state:
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

Tactic:
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root

Result:
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

Proof state:
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

Tactic:
rcases em (a = 0) with (rfl | ha)

Result:
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

Proof state:
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 < (C a * X + C b).natDegree
⊢ False

Tactic:
clear rid

Result:
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

Proof state:
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

Tactic:
simpa

Result:
no goals

Proof state:
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

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
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

Tactic:
obtain rfl : b = 0 := by simpa

Result:
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

Proof state:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
⊢ 1 < p.natDegree

Tactic:
by_contra rid

Result:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
rid : ¬1 < p.natDegree
⊢ False