awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
⊢ k > 0 ∧ ⌈(↑k : ℝ) * r⌉ - 1 = x ↔ k > 0 ∧ ⌊(↑k : ℝ) * r⌋ = x
have h : k > 0 → (⌈(↑k : ℝ) * r⌉ - 1 = x ↔ ⌊(↑k : ℝ) * r⌋ = x)
Tactic: rw [and_congr_right_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
⊢ ⌈(↑k : ℝ) * r⌉ - 1 = x ↔ ⌊(↑k : ℝ) * r⌋ = x
have h : ⌈(↑k : ℝ) * r⌉ - 1 = ⌊(↑k : ℝ) * r⌋
Tactic: congr!
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
⊢ ⌈(↑k : ℝ) * r⌉ - 1 = ⌊(↑k : ℝ) * r⌋
have h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) < (↑k : ℝ) * r ∧ (↑k : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑⌊(↑k : ℝ) * r⌋ : ℝ) 1
Tactic: rw [sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
⊢ (↑⌊(↑k : ℝ) * r⌋ : ℝ) < (↑k : ℝ) * r ∧ (↑k : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑⌊(↑k : ℝ) * r⌋ : ℝ) 1
have h : ∀ (h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) = (↑k : ℝ) * r), False
Tactic: refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
have rw : Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
Tactic: rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
rw : Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
have rw₁ : Eq (α := Set ℤ) {n : ℤ | 0 < n} {n : ℤ | 0 < n}
Tactic: rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : HPow.hPow (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C : ℚ } : ℝ) n = (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ False
have hxr₁ : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
Tactic: rw [← cast_pow] at hxr
Cleared hypotheses: hxr, hv
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ False
have c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
Tactic: have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
    rw [Int.cast_ne_zero, Int.natCast_ne_zero]
    exact P
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
⊢ False
have c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
Tactic: have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
⊢ False
have hxr₁ : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
Tactic: rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr
Cleared hypotheses: hxr, hv, c1, c2
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
⊢ False
have hdivn : HPow.hPow (α := ℤ) (↑D : ℤ) n ∣ N ^ n
Tactic: have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : HPow.hPow (α := ℤ) (↑D : ℤ) n ∣ N ^ n
⊢ False
have hdivn₁ : D ∣ N.natAbs
Tactic: rw [← Int.dvd_natAbs, ← Int.natCast_pow, Int.natCast_dvd_natCast, Int.natAbs_pow,
    Nat.pow_dvd_pow_iff hnpos.ne'] at hdivn
Cleared hypotheses: hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
⊢ D = 1
have rw : N.natAbs.gcd D = 1
Tactic: rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
rw : N.natAbs.gcd D = 1
⊢ D = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
⊢ False
have P₁ : Ne (α := ℕ) 1 0
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
⊢ False
have C₁ : N.natAbs.Coprime 1
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
C₁ : N.natAbs.Coprime 1
⊢ False
have hxr₁ : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
C₁ : N.natAbs.Coprime 1
hxr₁ : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
⊢ False
have hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P₁, reduced := C₁ } : ℝ) (↑y : ℝ)
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
C₁ : N.natAbs.Coprime 1
hxr₁ : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P₁, reduced := C₁ } : ℝ) (↑y : ℝ)
⊢ False
have c1₁ : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
C₁ : N.natAbs.Coprime 1
hxr₁ : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P₁, reduced := C₁ } : ℝ) (↑y : ℝ)
c1₁ : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
⊢ False
have c2₁ : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : D ∣ N.natAbs
P₁ : Ne (α := ℕ) 1 0
C₁ : N.natAbs.Coprime 1
hxr₁ : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P₁, reduced := C₁ } : ℝ) (↑y : ℝ)
c1₁ : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2₁ : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
⊢ False
have hdivn₁ : 1 ∣ N.natAbs
Tactic: obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
Cleared hypotheses: D, P, C, hxr, hv, c1, c2, hdivn
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : Ne (α := ℕ) 1 0
C : N.natAbs.Coprime 1
hxr : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
hdivn : 1 ∣ N.natAbs
⊢ False
have refine : Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
Tactic: refine hv ⟨N, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : Ne (α := ℕ) 1 0
C : N.natAbs.Coprime 1
hxr : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
hdivn : 1 ∣ N.natAbs
⊢ Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
have rw : Eq (α := ℝ) (↑(N /. (↑1 : ℤ)) : ℝ) (↑N : ℝ)
Tactic: rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : Ne (α := ℕ) 1 0
C : N.natAbs.Coprime 1
hxr : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
hdivn : 1 ∣ N.natAbs
rw : Eq (α := ℝ) (↑(N /. (↑1 : ℤ)) : ℝ) (↑N : ℝ)
⊢ Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
have rw₁ : Eq (α := ℝ) (↑(N /. 1) : ℝ) (↑N : ℝ)
Tactic: rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : Ne (α := ℕ) 1 0
C : N.natAbs.Coprime 1
hxr : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
hdivn : 1 ∣ N.natAbs
rw : Eq (α := ℝ) (↑(N /. (↑1 : ℤ)) : ℝ) (↑N : ℝ)
rw₁ : Eq (α := ℝ) (↑(N /. 1) : ℝ) (↑N : ℝ)
⊢ Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
have rw₂ : Eq (α := ℝ) (↑(↑N : ℚ) : ℝ) (↑N : ℝ)
Tactic: rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : Ne (α := ℕ) 1 0
C : N.natAbs.Coprime 1
hxr : m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0
hdivn : 1 ∣ N.natAbs
rw : Eq (α := ℝ) (↑(N /. (↑1 : ℤ)) : ℝ) (↑N : ℝ)
rw₁ : Eq (α := ℝ) (↑(N /. 1) : ℝ) (↑N : ℝ)
rw₂ : Eq (α := ℝ) (↑(↑N : ℚ) : ℝ) (↑N : ℝ)
⊢ Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
have rw₃ : Eq (α := ℝ) (↑N : ℝ) (↑N : ℝ)
Tactic: rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
⊢ Irrational x
have inl : ∀ (hxr : HPow.hPow (β := ℕ) x 0 = (↑m : ℝ)) (hv : multiplicity (↑p : ℤ) m % 0 ≠ 0), Irrational x
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
Cleared hypotheses: n, hxr, hv
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
inl : ∀ (hxr : HPow.hPow (β := ℕ) x 0 = (↑m : ℝ)) (hv : multiplicity (↑p : ℤ) m % 0 ≠ 0), Irrational x
⊢ Irrational x
have inr : ∀ (hnpos : n > 0), Irrational x
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : HPow.hPow (β := ℕ) x 0 = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % 0 ≠ 0
⊢ Irrational x
have hxr₁ : m = 1
Tactic: rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
Cleared hypotheses: hxr, hv
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x
have inr : ¬∃ (y : ℤ), x = (↑y : ℝ)
Tactic: refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : HPow.hPow (α := ℝ) (↑y : ℝ) n = (↑m : ℝ)
⊢ False
have hxr₁ : y ^ n = m
Tactic: rw [← Int.cast_pow, Int.cast_inj] at hxr
Cleared hypotheses: hxr
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
have hm₁ : y ^ n ≠ 0
Tactic: subst m
Cleared hypotheses: m, hm, hv, hxr
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p : ℤ) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
hm₁ : y ^ n ≠ 0
⊢ False
have hv₁ : multiplicity (↑p : ℤ) (y ^ n) % n ≠ 0
Tactic: subst m
Cleared hypotheses: m, hm, hv, hxr
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : HPow.hPow (α := ℤ) 0 n ≠ 0
hv : multiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) 0 n) % n ≠ 0
⊢ False
have hm₁ : Ne (α := ℤ) 0 0
Tactic: rw [zero_pow hnpos.ne'] at hm
Cleared hypotheses: hm, hv
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p : ℤ) (y ^ n) % n ≠ 0
⊢ False
have this : y ≠ 0
Tactic: have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (hypothesis)
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p : ℤ) (y ^ n) % n ≠ 0
this : y ≠ 0
⊢ False
have hv₁ : Ne (α := ℕ) 0 0
Tactic: rw [(Int.finiteMultiplicity_iff.2 ⟨by simp [hp.1.ne_one], this⟩).multiplicity_pow
    (Nat.prime_iff_prime_int.1 hp.1), Nat.mul_mod_right] at hv
Cleared hypotheses: hv, this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p : ℤ) m % 2 = 1
⊢ multiplicity (↑p : ℤ) m % 2 ≠ 0
have rw : Ne (α := ℕ) 1 0
Tactic: rw [Hpv]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q
have refine : (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) ↔ ∃ (r : ℚ), q = r * r
Tactic: refine Iff.not (?_ : Exists _ ↔ Exists _)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
⊢ (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) ↔ ∃ (r : ℚ), q = r * r
have mp : (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) → ∃ (r : ℚ), q = r * r
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
mp : (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) → ∃ (r : ℚ), q = r * r
⊢ (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) ↔ ∃ (r : ℚ), q = r * r
have mpr : (∃ (r : ℚ), q = r * r) → ∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
⊢ ∃ (r : ℚ), q = r * r
have mp : Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)
Tactic: refine ⟨y, Rat.cast_injective (α := ℝ) ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
⊢ Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)
have mp : (↑q : ℝ) = HMul.hMul (α := ℝ) (↑y : ℝ) (↑y : ℝ)
Tactic: rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
mp : (↑q : ℝ) = HMul.hMul (α := ℝ) (↑y : ℝ) (↑y : ℝ)
⊢ Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)
have mp₁ : (↑q : ℝ) = √(↑q : ℝ) * √(↑q : ℝ)
Tactic: rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
mp : (↑q : ℝ) = HMul.hMul (α := ℝ) (↑y : ℝ) (↑y : ℝ)
mp₁ : (↑q : ℝ) = √(↑q : ℝ) * √(↑q : ℝ)
⊢ Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)
have mp₂ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
Tactic: rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
have inl : ∀ (hq : 0 ≤ q), Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
Tactic: obtain hq | hq := le_or_gt 0 q
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
inl : ∀ (hq : 0 ≤ q), Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
have inr : ∀ (hq : q < 0), Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
Tactic: obtain hq | hq := le_or_gt 0 q
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
have inl : ¬IsSquare q ↔ ¬IsSquare q ∧ 0 ≤ q
Tactic: simp_rw [irrational_sqrt_ratCast_iff_of_nonneg hq, and_iff_left hq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
have inr : Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
Tactic: rw [sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 hq.le)]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
have inr : False ↔ ¬IsSquare q ∧ 0 ≤ q
Tactic: simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
inr : False ↔ ¬IsSquare q ∧ 0 ≤ q
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
have inr₁ : ¬(¬IsSquare q ∧ 0 ≤ q)
Tactic: simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
inr : False ↔ ¬IsSquare q ∧ 0 ≤ q
inr₁ : ¬(¬IsSquare q ∧ 0 ≤ q)
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
have inr₂ : ¬IsSquare q → ¬0 ≤ q
Tactic: simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
inr : False ↔ ¬IsSquare q ∧ 0 ≤ q
inr₁ : ¬(¬IsSquare q ∧ 0 ≤ q)
inr₂ : ¬IsSquare q → ¬0 ≤ q
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
have inr₃ : ¬IsSquare q → q < 0
Tactic: simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
q : ℚ
hq : q < 0
inr : False ↔ ¬IsSquare q ∧ 0 ≤ q
inr₁ : ¬(¬IsSquare q ∧ 0 ≤ q)
inr₂ : ¬IsSquare q → ¬0 ≤ q
inr₃ : ¬IsSquare q → q < 0
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
have inr₄ : ¬IsSquare q → True
Tactic: simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
hz : 0 ≤ z
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z
have rw : Irrational √(↑z : ℝ) ↔ ¬IsSquare (α := ℚ) (↑z : ℚ)
Tactic: rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz),
    Rat.cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
hz : 0 ≤ z
rw : Irrational √(↑z : ℝ) ↔ ¬IsSquare (α := ℚ) (↑z : ℚ)
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z
have rw₁ : Irrational √(↑z : ℝ) ↔ Irrational √(↑(↑z : ℚ) : ℝ)
Tactic: rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz),
    Rat.cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
hz : 0 ≤ z
rw : Irrational √(↑z : ℝ) ↔ ¬IsSquare (α := ℚ) (↑z : ℚ)
rw₁ : Irrational √(↑z : ℝ) ↔ Irrational √(↑(↑z : ℚ) : ℝ)
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z
have rw₂ : Irrational √(↑z : ℝ) ↔ Irrational √(↑z : ℝ)
Tactic: rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz),
    Rat.cast_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
z : ℤ
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z
have rw : Irrational √(↑(↑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
⊢ 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]