awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
rw : Irrational √(↑(↑z : ℚ) : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z
rw₁ : ¬IsSquare (α := ℚ) (↑z : ℚ) ∧ LE.le (α := ℚ) 0 (↑z : ℚ) ↔ ¬IsSquare z ∧ 0 ≤ z
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z
have rw₂ : ¬IsSquare z ∧ LE.le (α := ℚ) 0 (↑z : ℚ) ↔ ¬IsSquare z ∧ 0 ≤ z
Tactic: rw [← Rat.cast_intCast, irrational_sqrt_ratCast_iff, Rat.isSquare_intCast_iff,
    Int.cast_nonneg_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
rw : Irrational √(↑(↑z : ℚ) : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z
rw₁ : ¬IsSquare (α := ℚ) (↑z : ℚ) ∧ LE.le (α := ℚ) 0 (↑z : ℚ) ↔ ¬IsSquare z ∧ 0 ≤ z
rw₂ : ¬IsSquare z ∧ LE.le (α := ℚ) 0 (↑z : ℚ) ↔ ¬IsSquare z ∧ 0 ≤ z
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z
have rw₃ : ¬IsSquare z ∧ 0 ≤ z ↔ ¬IsSquare z ∧ 0 ≤ z
Tactic: rw [← Rat.cast_intCast, irrational_sqrt_ratCast_iff, Rat.isSquare_intCast_iff,
    Int.cast_nonneg_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
⊢ Irrational √(↑n : ℝ) ↔ ¬IsSquare n
have rw : Irrational √(↑n : ℝ) ↔ ¬IsSquare (α := ℚ) (↑n : ℚ)
Tactic: rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
    Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
rw : Irrational √(↑n : ℝ) ↔ ¬IsSquare (α := ℚ) (↑n : ℚ)
⊢ Irrational √(↑n : ℝ) ↔ ¬IsSquare n
have rw₁ : Irrational √(↑n : ℝ) ↔ Irrational √(↑(↑n : ℚ) : ℝ)
Tactic: rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
    Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
rw : Irrational √(↑n : ℝ) ↔ ¬IsSquare (α := ℚ) (↑n : ℚ)
rw₁ : Irrational √(↑n : ℝ) ↔ Irrational √(↑(↑n : ℚ) : ℝ)
⊢ Irrational √(↑n : ℝ) ↔ ¬IsSquare n
have rw₂ : Irrational √(↑n : ℝ) ↔ Irrational √(↑n : ℝ)
Tactic: rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
    Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x y : ℝ
⊢ x + y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast
have 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)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational ((↑(-q) : ℝ) + ((↑q : ℝ) + x))
have rwa : Irrational (-(↑q : ℝ) + ((↑q : ℝ) + x))
Tactic: rwa [cast_neg, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑m : ℝ) + x)
⊢ Irrational x
have h₁ : Irrational ((↑(↑m : ℚ) : ℝ) + x)
Tactic: rw [← cast_intCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational (-x)
h_1 : Membership.mem (γ := Set ℝ) (Set.range Rat.cast) x
q : ℚ
hx : (↑q : ℝ) = x
⊢ (↑(-q) : ℝ) = -x
have rw : -(↑q : ℝ) = -x
Tactic: rw [cast_neg, hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational (-x)
h_1 : Membership.mem (γ := Set ℝ) (Set.range Rat.cast) x
q : ℚ
hx : (↑q : ℝ) = x
rw : -(↑q : ℝ) = -x
⊢ (↑(-q) : ℝ) = -x
have rw₁ : -x = -x
Tactic: rw [cast_neg, hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x y : ℝ
⊢ x * y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast
have 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)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * (↑q : ℝ) * (↑q⁻¹ : ℝ))
have rwa : Irrational (x * HMul.hMul (α := ℝ) (↑q : ℝ) (↑q⁻¹ : ℝ))
Tactic: rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
rwa : Irrational (x * HMul.hMul (α := ℝ) (↑q : ℝ) (↑q⁻¹ : ℝ))
⊢ Irrational (x * (↑q : ℝ) * (↑q⁻¹ : ℝ))
have rwa₁ : Irrational (x * (↑(q * q⁻¹) : ℝ))
Tactic: rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
rwa : Irrational (x * HMul.hMul (α := ℝ) (↑q : ℝ) (↑q⁻¹ : ℝ))
rwa₁ : Irrational (x * (↑(q * q⁻¹) : ℝ))
⊢ Irrational (x * (↑q : ℝ) * (↑q⁻¹ : ℝ))
have rwa₂ : Irrational (x * (↑1 : ℝ))
Tactic: rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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 : ℝ))
⊢ Irrational (x * (↑q : ℝ) * (↑q⁻¹ : ℝ))
have rwa₃ : Irrational (x * 1)
Tactic: rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * (↑(↑m : ℚ) : ℝ))
have refine : Ne (α := ℚ) (↑m : ℚ) 0
Tactic: refine h.mul_ratCast ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / (↑q : ℝ))
have rw : Irrational (x * (↑q⁻¹ : ℝ))
Tactic: rw [div_eq_mul_inv, ← cast_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / (↑(↑m : ℚ) : ℝ))
have refine : Ne (α := ℚ) (↑m : ℚ) 0
Tactic: refine h.div_ratCast ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
h : Irrational (HPow.hPow (β := ℕ) x 0)
⊢ Irrational x
have h₁ : Irrational 1
Tactic: rw [pow_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x
have h₁ : Irrational (x ^ n * x)
Tactic: rw [pow_succ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
n : ℕ
h : Irrational (HPow.hPow (β := ℤ) x (↑n : ℤ))
⊢ Irrational x
have h₁ : Irrational (x ^ n)
Tactic: rw [zpow_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x
have h₁ : Irrational (x ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) p : ℝ) (0 : ℝ)
⊢ 1 < p.natDegree
have by_contra : ∀ (rid : ¬1 < p.natDegree), False
Tactic: by_contra rid
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
⊢ False
have 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
Tactic: rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
Cleared hypotheses: p, p_nonzero, x_is_root, rid
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
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 : ℝ)
⊢ False
have this : (↑a : ℝ) * x = -(↑b : ℝ)
Tactic: have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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 : ℝ)
⊢ False
have 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
Tactic: rcases em (a = 0) with (rfl | ha)
Cleared hypotheses: a, p_nonzero, x_is_root, this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
⊢ False
have inr : ∀ (ha : ¬a = 0), False
Tactic: rcases em (a = 0) with (rfl | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
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 : ℝ)
⊢ False
have p_nonzero₁ : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 0) X + (C : (a : ℤ) → ℤ[X]) 0 ≠ 0
Tactic: obtain rfl : b = 0 := by simpa
Cleared hypotheses: b, p_nonzero, x_is_root, this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
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
⊢ False
have x_is_root₁ : 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
Cleared hypotheses: b, p_nonzero, x_is_root, this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
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 : ℝ)
⊢ False
have this₁ : (↑0 : ℝ) * x = -(↑0 : ℝ)
Tactic: obtain rfl : b = 0 := by simpa
Cleared hypotheses: b, p_nonzero, x_is_root, this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
⊢ False
have inr : ∀ (this : HDiv.hDiv (α := ℝ) (-(↑b : ℝ)) (↑a : ℝ) = x) (ha : ¬a = 0), False
Tactic: rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
Cleared hypotheses: this, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
⊢ False
have inr₁ : ∀ (this : x * (↑a : ℝ) = -(↑b : ℝ)) (ha : ¬a = 0), Ne (α := ℝ) (↑a : ℝ) 0
Tactic: rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
Cleared hypotheses: this, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
have inr : (↑(HDiv.hDiv (α := ℚ) (-(↑b : ℚ)) (↑a : ℚ)) : ℝ) = x
Tactic: refine hx ⟨-b / a, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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
⊢ (↑(HDiv.hDiv (α := ℚ) (-(↑b : ℚ)) (↑a : ℚ)) : ℝ) = x
have 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
Tactic: assumption_mod_cast
Cleared hypotheses: p_nonzero, x_is_root, this, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
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 : x * (↑a : ℝ) = -(↑b : ℝ)
ha : ¬a = 0
⊢ Ne (α := ℝ) (↑a : ℝ) 0
have 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 : x * (↑a : ℝ) = (↑(-b) : ℝ)) (ha : ¬a = 0), ¬a = 0
Tactic: assumption_mod_cast
Cleared hypotheses: p_nonzero, x_is_root, this, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
⊢ Irrational (x * (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw : Irrational ((↑q : ℝ) * x) ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [mul_comm, irrational_ratCast_mul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
rw : Irrational ((↑q : ℝ) * x) ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw₁ : q ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [mul_comm, irrational_ratCast_mul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
⊢ Irrational ((↑m : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
have rw : Irrational ((↑(↑m : ℚ) : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational ((↑(↑m : ℚ) : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational ((↑m : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational ((↑(↑m : ℚ) : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational ((↑m : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
have rw₂ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
⊢ Irrational (x * (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw : Irrational (x * (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_mul_ratCast_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational (x * (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_mul_ratCast_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational (x * (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw₂ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_mul_ratCast_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
⊢ Irrational ((↑n : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
have rw : Irrational ((↑(↑n : ℚ) : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational ((↑(↑n : ℚ) : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational ((↑n : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational ((↑(↑n : ℚ) : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational ((↑n : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
have rw₂ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
⊢ Irrational (x * (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw : Irrational (x * (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_mul_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational (x * (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_mul_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational (x * (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw₂ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_mul_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw₁ : Irrational (x * (↑q⁻¹ : ℝ)) ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
rw₁ : Irrational (x * (↑q⁻¹ : ℝ)) ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw₂ : q⁻¹ ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
rw₁ : Irrational (x * (↑q⁻¹ : ℝ)) ↔ q ≠ 0 ∧ Irrational x
rw₂ : q⁻¹ ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw₃ : ¬q⁻¹ = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
x : ℝ
rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
rw₁ : Irrational (x * (↑q⁻¹ : ℝ)) ↔ q ≠ 0 ∧ Irrational x
rw₂ : q⁻¹ ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
rw₃ : ¬q⁻¹ = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x
have rw₄ : ¬q = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
Tactic: rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
⊢ Irrational (x / (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw : Irrational (x / (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero]