awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational ((↑m : ℝ) + x)
⊢ Irrational x

Tactic:
h.of_intCast_add m

Premises used: Nat.cast, Irrational.of_intCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational (x + (↑m : ℝ))
⊢ Irrational x

Tactic:
h.of_add_intCast m

Premises used: Nat.cast, Irrational.of_add_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
⊢ Irrational ((↑m : ℝ) + x)

Tactic:
h.intCast_add m

Premises used: Irrational.intCast_add, Nat.cast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
⊢ Irrational (x + (↑m : ℝ))

Tactic:
h.add_intCast m

Premises used: Nat.cast, Irrational.add_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational (-x)
h_1 : Membership.mem (γ := Set ℝ) (Set.range Rat.cast) x
q : ℚ
hx : (↑q : ℝ) = x
rw : -(↑q : ℝ) = -x
rw₁ rw₂ : -x = -x
⊢ (↑(-q) : ℝ) = -x

Tactic:
rw [cast_neg, hx]

Premises used: Rat.cast_neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h rwa rwa₁ rwa₂ rwa₃ : Irrational x
⊢ Irrational (- -x)

Tactic:
rwa [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x - (↑q : ℝ))

Tactic:
simpa only [sub_eq_add_neg, cast_neg] using h.add_ratCast (-q)

Premises used: sub_eq_add_neg, Irrational.add_ratCast, Rat.cast_neg, Neg.neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational ((↑q : ℝ) - x)

Tactic:
simpa only [sub_eq_add_neg] using h.neg.ratCast_add q

Premises used: Irrational.neg, sub_eq_add_neg, Irrational.ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational (x - (↑q : ℝ))
⊢ Irrational (x + (↑(-q) : ℝ))

Tactic:
simpa only [cast_neg, sub_eq_add_neg] using h

Premises used: sub_eq_add_neg, Rat.cast_neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational ((↑q : ℝ) - x)
⊢ Irrational ((↑q : ℝ) + -x)

Tactic:
simpa only [sub_eq_add_neg] using h

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - (↑m : ℝ))

Tactic:
simpa only [Rat.cast_intCast] using h.sub_ratCast m

Premises used: Int.cast, Rat.cast_intCast, Irrational.sub_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational ((↑m : ℝ) - x)

Tactic:
simpa only [Rat.cast_intCast] using h.ratCast_sub m

Premises used: Int.cast, Irrational.ratCast_sub, Rat.cast_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational (x - (↑m : ℝ))
rwa rwa₁ rwa₂ rwa₃ : Irrational (x - (↑m : ℝ))
⊢ Irrational (x - (↑(↑m : ℚ) : ℝ))

Tactic:
rwa [Rat.cast_intCast]

Premises used: Rat.cast_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑m : ℝ) - x)
rwa rwa₁ rwa₂ rwa₃ : Irrational ((↑m : ℝ) - x)
⊢ Irrational ((↑(↑m : ℚ) : ℝ) - x)

Tactic:
rwa [Rat.cast_intCast]

Premises used: Rat.cast_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
⊢ Irrational (x - (↑m : ℝ))

Tactic:
h.sub_intCast m

Premises used: Nat.cast, Irrational.sub_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
⊢ Irrational ((↑m : ℝ) - x)

Tactic:
h.intCast_sub m

Premises used: Nat.cast, Irrational.intCast_sub
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational (x - (↑m : ℝ))
⊢ Irrational x

Tactic:
h.of_sub_intCast m

Premises used: Nat.cast, Irrational.of_sub_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational ((↑m : ℝ) - x)
⊢ Irrational x

Tactic:
h.of_intCast_sub m

Premises used: Irrational.of_intCast_sub, Nat.cast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x y : ℝ
contrapose! :
  Membership.mem (γ := Set ℝ) (Set.range Rat.cast) x ∧ Membership.mem (γ := Set ℝ) (Set.range Rat.cast) y →
    Membership.mem (γ := Set ℝ) (Set.range Rat.cast) (x * y)
⊢ x * y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
rx ry : ℚ
⊢ Membership.mem (γ := Set ℝ) (Set.range Rat.cast) (HMul.hMul (α := ℝ) (↑rx : ℝ) (↑ry : ℝ))

Tactic:
⟨rx * ry, cast_mul rx ry⟩

Premises used: Rat.cast_mul, HMul.hMul, Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
rx ry : ℚ
⊢ Membership.mem (γ := Set ℝ) (Set.range Rat.cast) (HMul.hMul (α := ℝ) (↑rx : ℝ) (↑ry : ℝ))

Tactic:
exact ⟨rx * ry, cast_mul rx ry⟩
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational (x * (↑q : ℝ))
⊢ Irrational x

Tactic:
h.mul_cases.resolve_right q.not_irrational

Premises used: Rat.not_irrational, Irrational.mul_cases, Or.resolve_right
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
rwa : Irrational (x * HMul.hMul (α := ℝ) (↑q : ℝ) (↑q⁻¹ : ℝ))
rwa₁ : Irrational (x * (↑(q * q⁻¹) : ℝ))
rwa₂ : Irrational (x * (↑1 : ℝ))
rwa₃ : Irrational (x * 1)
rwa₄ rwa₅ rwa₆ rwa₇ : Irrational x
⊢ Irrational (x * (↑q : ℝ) * (↑q⁻¹ : ℝ))

Tactic:
rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]

Premises used: Rat.cast_mul, mul_inv_cancel₀, mul_assoc, mul_one, Rat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational ((↑q : ℝ) * x) → Irrational x

Tactic:
mul_comm x q ▸ of_mul_ratCast q

Premises used: Eq.rec, Rat.cast, Irrational.of_mul_ratCast, mul_comm
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational ((↑q : ℝ) * x)

Tactic:
mul_comm x q ▸ h.mul_ratCast hq

Premises used: Eq.rec, Rat.cast, mul_comm, Irrational.mul_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational (x * (↑m : ℝ))
rwa rwa₁ rwa₂ rwa₃ : Irrational (x * (↑m : ℝ))
⊢ Irrational (x * (↑(↑m : ℚ) : ℝ))

Tactic:
rwa [cast_intCast]

Premises used: Rat.cast_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑m : ℝ) * x)
rwa rwa₁ rwa₂ rwa₃ : Irrational ((↑m : ℝ) * x)
⊢ Irrational ((↑(↑m : ℚ) : ℝ) * x)

Tactic:
rwa [cast_intCast]

Premises used: Rat.cast_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * (↑(↑m : ℚ) : ℝ))

Tactic:
h.mul_ratCast ?_

Premises used: Irrational.mul_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
refine : Ne (α := ℚ) (↑m : ℚ) 0
⊢ Irrational (x * (↑(↑m : ℚ) : ℝ))

Tactic:
refine h.mul_ratCast ?_

Premises used: Irrational.mul_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm rwa rwa₁ rwa₂ rwa₃ : m ≠ 0
⊢ Ne (α := ℚ) (↑m : ℚ) 0

Tactic:
rwa [Int.cast_ne_zero]

Premises used: Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational ((↑m : ℝ) * x)

Tactic:
mul_comm x m ▸ h.mul_intCast hm

Premises used: Int.cast, Irrational.mul_intCast, Eq.rec, mul_comm
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational (x * (↑m : ℝ))
⊢ Irrational x

Tactic:
h.of_mul_intCast m

Premises used: Nat.cast, Irrational.of_mul_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational ((↑m : ℝ) * x)
⊢ Irrational x

Tactic:
h.of_intCast_mul m

Premises used: Irrational.of_intCast_mul, Nat.cast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ Irrational (x * (↑m : ℝ))

Tactic:
h.mul_intCast <| Int.natCast_ne_zero.2 hm

Premises used: Iff.mpr, Int.natCast_ne_zero, Irrational.mul_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ Irrational ((↑m : ℝ) * x)

Tactic:
h.intCast_mul <| Int.natCast_ne_zero.2 hm

Premises used: Iff.mpr, Int.natCast_ne_zero, Irrational.intCast_mul
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x⁻¹
⊢ Irrational x

Tactic:
fun ⟨q, hq⟩ => h <| hq ▸ ⟨q⁻¹, q.cast_inv⟩

Premises used: False, Eq.rec, _private.0.Irrational.of_neg.match_1, Rat.cast_inv, Inv.inv, Irrational, Exists.intro, Not
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h rwa rwa₁ rwa₂ rwa₃ : Irrational x
⊢ Irrational x⁻¹⁻¹

Tactic:
rwa [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x y : ℝ
h : Irrational (x / y)
⊢ Irrational x ∨ Irrational y

Tactic:
h.mul_cases.imp id of_inv

Premises used: id, Irrational.of_inv, Irrational.mul_cases, Or.imp
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational ((↑q : ℝ) / x)
⊢ Irrational x

Tactic:
(h.of_ratCast_mul q).of_inv

Premises used: Irrational.of_ratCast_mul, Irrational.of_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational (x / (↑q : ℝ))
⊢ Irrational x

Tactic:
h.div_cases.resolve_right q.not_irrational

Premises used: Irrational.div_cases, Rat.not_irrational, Or.resolve_right
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational ((↑q : ℝ) / x)

Tactic:
h.inv.ratCast_mul hq

Premises used: Irrational.ratCast_mul, Irrational.inv, DivInvMonoid.div'
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
rw : Irrational (x * (↑q⁻¹ : ℝ))
⊢ Irrational (x / (↑q : ℝ))

Tactic:
rw [div_eq_mul_inv, ← cast_inv]

Premises used: div_eq_mul_inv, Rat.cast_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * (↑q⁻¹ : ℝ))

Tactic:
h.mul_ratCast (inv_ne_zero hq)

Premises used: inv_ne_zero, Irrational.mul_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * (↑q⁻¹ : ℝ))

Tactic:
exact h.mul_ratCast (inv_ne_zero hq)

Premises used: inv_ne_zero, Irrational.mul_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑m : ℝ) / x)
⊢ Irrational x

Tactic:
h.div_cases.resolve_left m.not_irrational

Premises used: Irrational.div_cases, Or.resolve_left, Int.not_irrational
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational (x / (↑m : ℝ))
⊢ Irrational x

Tactic:
h.div_cases.resolve_right m.not_irrational

Premises used: Irrational.div_cases, Int.not_irrational, Or.resolve_right
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational ((↑m : ℝ) / x)

Tactic:
h.inv.intCast_mul hm

Premises used: Irrational.intCast_mul, Irrational.inv, DivInvMonoid.div'
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / (↑(↑m : ℚ) : ℝ))

Tactic:
h.div_ratCast ?_

Premises used: Irrational.div_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
refine : Ne (α := ℚ) (↑m : ℚ) 0
⊢ Irrational (x / (↑(↑m : ℚ) : ℝ))

Tactic:
refine h.div_ratCast ?_

Premises used: Irrational.div_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational ((↑m : ℝ) / x)
⊢ Irrational x

Tactic:
h.of_intCast_div m

Premises used: Irrational.of_intCast_div, Nat.cast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℕ
h : Irrational (x / (↑m : ℝ))
⊢ Irrational x

Tactic:
h.of_div_intCast m

Premises used: Nat.cast, Irrational.of_div_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ Irrational ((↑m : ℝ) / x)

Tactic:
h.inv.natCast_mul hm

Premises used: Irrational.inv, DivInvMonoid.div', Irrational.natCast_mul
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℕ
hm rwa rwa₁ rwa₂ rwa₃ : m ≠ 0
⊢ Ne (α := ℤ) (↑m : ℤ) 0

Tactic:
rwa [Int.natCast_ne_zero]

Premises used: Int.natCast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational (1 / x)
rwa rwa₁ rwa₂ rwa₃ : Irrational (1 / x)
⊢ Irrational ((↑1 : ℝ) / x)

Tactic:
rwa [cast_one]

Premises used: Rat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational (x * x)
⊢ Irrational x

Tactic:
h.mul_cases.elim id id

Premises used: id, Irrational.mul_cases, Or.elim
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational (HPow.hPow (β := ℕ) x 0)
⊢ Irrational 1

Tactic:
rw [pow_zero] at h

Premises used: pow_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational 1
⊢ Irrational x

Tactic:
(h ⟨1, cast_one⟩).elim

Premises used: False.elim, Exists.intro, OfNat.ofNat, Rat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational 1
⊢ Irrational x

Tactic:
exact (h ⟨1, cast_one⟩).elim

Premises used: False.elim, Exists.intro, OfNat.ofNat, Rat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational (x ^ n * x)

Tactic:
rw [pow_succ] at h

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x

Tactic:
h.mul_cases.elim (of_pow n) id

Premises used: id, Irrational.mul_cases, Or.elim
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x

Tactic:
exact h.mul_cases.elim (of_pow n) id

Premises used: id, Irrational.mul_cases, Or.elim
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (HPow.hPow (β := ℤ) x (↑n : ℤ))
⊢ Irrational (x ^ n)

Tactic:
rw [zpow_natCast] at h

Premises used: zpow_natCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x

Tactic:
h.of_pow _

Premises used: Irrational.of_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x

Tactic:
exact h.of_pow _

Premises used: Irrational.of_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational (x ^ (n + 1))⁻¹

Tactic:
rw [zpow_negSucc] at h

Premises used: zpow_negSucc
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x

Tactic:
h.of_inv.of_pow _

Premises used: Irrational.of_pow, Irrational.of_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x

Tactic:
exact h.of_inv.of_pow _

Premises used: Irrational.of_pow, Irrational.of_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) p : ℝ) (0 : ℝ)
by_contra : ∀ (rid : ¬1 < p.natDegree), False
⊢ 1 < p.natDegree

Tactic:
by_contra rid
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) p : ℝ) (0 : ℝ)
rid : ¬1 < p.natDegree
rcases :
  ∀ (a b : ℤ)
    (p_nonzero :
      HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
        0)
    (x_is_root :
      Eq (α := ℝ)
        ((aeval x : (a : ℤ[X]) → ℝ)
            (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
              ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
          ℝ)
        (0 : ℝ))
    (rid :
      ¬1 <
          (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
              ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])).natDegree),
    False
⊢ False

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

Premises used: Polynomial.exists_eq_X_add_C_of_natDegree_le_one, not_lt, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
⊢ (↑a : ℝ) * x = -(↑b : ℝ)

Tactic:
simpa [eq_neg_iff_add_eq_zero] using x_is_root

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
⊢ (↑a : ℝ) * x = -(↑b : ℝ)

Tactic:
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑a : ℝ) * x = -(↑b : ℝ)
inl :
  ∀
    (p_nonzero :
      HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠ 0)
    (x_is_root :
      Eq (α := ℝ)
        ((aeval x : (a : ℤ[X]) → ℝ)
            (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
          ℝ)
        (0 : ℝ))
    (this : (↑0 : ℝ) * x = -(↑b : ℝ)), False
inr : ∀ (ha : ¬a = 0), False
⊢ False

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

Premises used: em, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠ 0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑0 : ℝ) * x = -(↑b : ℝ)
⊢ b = 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠ 0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑0 : ℝ) * x = -(↑b : ℝ)
⊢ HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0 ≠ 0

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

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠ 0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑0 : ℝ) * x = -(↑b : ℝ)
p_nonzero₁ : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0 ≠ 0
⊢ Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0) : ℝ) (0 : ℝ)

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

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠ 0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X) ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑0 : ℝ) * x = -(↑b : ℝ)
p_nonzero₁ : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0 ≠ 0
x_is_root₁ :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0) : ℝ) (0 : ℝ)
⊢ (↑0 : ℝ) * x = -(↑0 : ℝ)

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

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
p_nonzero : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0 ≠ 0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ) (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0) : ℝ) (0 : ℝ)
this : (↑0 : ℝ) * x = -(↑0 : ℝ)
⊢ False

Tactic:
simp at p_nonzero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : (↑a : ℝ) * x = -(↑b : ℝ)
ha : ¬a = 0
inr : ∀ (this : HDiv.hDiv (α := ℝ) (-(↑b : ℝ)) (↑a : ℝ) = x) (ha : ¬a = 0), False
inr₁ : ∀ (this : x * (↑a : ℝ) = -(↑b : ℝ)) (ha : ¬a = 0), Ne (α := ℝ) (↑a : ℝ) 0
⊢ False

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

Premises used: eq_comm, eq_div_iff_mul_eq, mul_comm
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : HDiv.hDiv (α := ℝ) (-(↑b : ℝ)) (↑a : ℝ) = x
ha : ¬a = 0
⊢ False

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

Premises used: Int.cast, HDiv.hDiv, Exists.intro, Neg.neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : HDiv.hDiv (α := ℝ) (-(↑b : ℝ)) (↑a : ℝ) = x
ha : ¬a = 0
inr : (↑(HDiv.hDiv (α := ℚ) (-(↑b : ℚ)) (↑a : ℚ)) : ℝ) = x
⊢ False

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

Premises used: Int.cast, HDiv.hDiv, Exists.intro, Neg.neg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : HDiv.hDiv (α := ℝ) (-(↑b : ℝ)) (↑a : ℝ) = x
ha : ¬a = 0
inr inr₁ inr₂ inr₃ :
  ∀
    (p_nonzero :
      ¬HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
            ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) =
          0)
    (x_is_root :
      Eq (α := ℝ)
        ((aeval x : (a : ℤ[X]) → ℝ)
            (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
              ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
          ℝ)
        (0 : ℝ))
    (this : (↑(-b /. a) : ℝ) = x) (ha : ¬a = 0), (↑(-b /. a) : ℝ) = x
⊢ (↑(HDiv.hDiv (α := ℚ) (-(↑b : ℚ)) (↑a : ℚ)) : ℝ) = x

Tactic:
assumption_mod_cast