awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Real.Irrational
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
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ D = 1

Tactic:
rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: Nat.Coprime.gcd_eq_one, Nat.gcd_eq_right
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ Ne (α := ℕ) 1 0

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ N.natAbs.Coprime 1

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ m * HPow.hPow (α := ℤ) (↑1 : ℤ) n = N ^ n

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ ¬∃ (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]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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 : ℝ)
⊢ Ne (α := ℝ) (↑(↑1 : ℤ) : ℝ) 0

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ HPow.hPow (α := ℝ) (↑(↑1 : ℤ) : ℝ) n ≠ 0

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ 1 ∣ N.natAbs

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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

Tactic:
hv ⟨N, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
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
refine : Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)
⊢ False

Tactic:
refine hv ⟨N, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
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 : ℝ)
rw₃ rw₄ : Eq (α := ℝ) (↑N : ℝ) (↑N : ℝ)
⊢ Eq (α := ℝ) (↑{ num := N, den_nz := P, reduced := C } : ℝ) (↑N : ℝ)

Tactic:
rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]

Premises used: Rat.cast_intCast, Rat.mk_eq_divInt, Rat.divInt_one, Int.ofNat_one
-- Module: Mathlib.NumberTheory.Real.Irrational
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
inr : ∀ (hnpos : n > 0), Irrational x
⊢ Irrational x

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : HPow.hPow (β := ℕ) x 0 = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % 0 ≠ 0
⊢ m = 1

Tactic:
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr

Premises used: Int.cast_inj, eq_comm, pow_zero, Int.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : HPow.hPow (β := ℕ) x 0 = (↑m : ℝ)
hv : multiplicity (↑p : ℤ) m % 0 ≠ 0
hxr₁ : m = 1
⊢ multiplicity (↑p : ℤ) m % 0 ≠ 0

Tactic:
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr

Premises used: Int.cast_inj, eq_comm, pow_zero, Int.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p : ℤ) m % 0 ≠ 0
⊢ Irrational x

Tactic:
simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv

Premises used: mt, Iff.mp, Nat.Prime.not_dvd_one, isUnit_iff_dvd_one, Fact.out, multiplicity_of_one_right, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Real.Irrational
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

Tactic:
irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos

Premises used: irrational_nrt_of_notint_nrt
-- Module: Mathlib.NumberTheory.Real.Irrational
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
inr : ¬∃ (y : ℤ), x = (↑y : ℝ)
⊢ Irrational x

Tactic:
refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos

Premises used: irrational_nrt_of_notint_nrt
-- Module: Mathlib.NumberTheory.Real.Irrational
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 : ℝ)
⊢ y ^ n = m

Tactic:
rw [← Int.cast_pow, Int.cast_inj] at hxr

Premises used: Int.cast_inj, Int.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ y ^ n ≠ 0

Tactic:
subst m
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ multiplicity (↑p : ℤ) (y ^ n) % n ≠ 0

Tactic:
subst m
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ Ne (α := ℤ) 0 0

Tactic:
rw [zero_pow hnpos.ne'] at hm

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
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
hm₁ : Ne (α := ℤ) 0 0
⊢ multiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) 0 n) % n ≠ 0

Tactic:
rw [zero_pow hnpos.ne'] at hm

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : Ne (α := ℤ) 0 0
hv : multiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) 0 n) % n ≠ 0
⊢ False

Tactic:
hm rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : Ne (α := ℤ) 0 0
hv : multiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) 0 n) % n ≠ 0
⊢ False

Tactic:
exact hm rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p : ℤ) (y ^ n) % n ≠ 0
⊢ y ≠ 0

Tactic:
have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ Int.natAbs (↑p : ℤ) ≠ 1

Tactic:
simp [hp.1.ne_one]

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Real.Irrational
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
⊢ 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

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Int.finiteMultiplicity_iff, FiniteMultiplicity.multiplicity_pow, And.intro, Iff.mp, Nat.mul_mod_right, Fact.out
-- Module: Mathlib.NumberTheory.Real.Irrational
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
hv₁ : Ne (α := ℕ) 0 0
⊢ y ≠ 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

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Int.finiteMultiplicity_iff, FiniteMultiplicity.multiplicity_pow, And.intro, Iff.mp, Nat.mul_mod_right, Fact.out
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Ne (α := ℕ) 0 0
this : y ≠ 0
⊢ False

Tactic:
hv rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Ne (α := ℕ) 0 0
this : y ≠ 0
⊢ False

Tactic:
exact hv rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p : ℤ) m % 2 = 1
rw : Ne (α := ℕ) 1 0
⊢ multiplicity (↑p : ℤ) m % 2 ≠ 0

Tactic:
rw [Hpv]
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p : ℤ) m % 2 = 1
⊢ Ne (α := ℕ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p : ℤ) m % 2 = 1
⊢ Ne (α := ℕ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
⊢ ¬Irrational 0

Tactic:
not_not_intro ⟨0, Rat.cast_zero⟩

Premises used: not_not_intro, Irrational, Exists.intro, Rat.cast_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
⊢ ¬Irrational 1

Tactic:
not_not_intro ⟨1, Rat.cast_one⟩

Premises used: not_not_intro, Irrational, Exists.intro, OfNat.ofNat, Rat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q

Tactic:
Iff.not (?_ : Exists _ ↔ Exists _)

Premises used: Iff.not, Irrational
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
refine : (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) ↔ ∃ (r : ℚ), q = r * r
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q

Tactic:
refine Iff.not (?_ : Exists _ ↔ Exists _)

Premises used: Iff.not
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
mp : (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) → ∃ (r : ℚ), q = r * r
mpr : (∃ (r : ℚ), q = r * r) → ∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)
⊢ (∃ (y : ℚ), (↑y : ℝ) = √(↑q : ℝ)) ↔ ∃ (r : ℚ), q = r * r

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
⊢ ∃ (r : ℚ), q = r * r

Tactic:
⟨y, Rat.cast_injective (α := ℝ) ?_⟩

Premises used: Exists.intro, Rat.cast_injective
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
mp : Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)
⊢ ∃ (r : ℚ), q = r * r

Tactic:
refine ⟨y, Rat.cast_injective (α := ℝ) ?_⟩
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : (↑y : ℝ) = √(↑q : ℝ)
mp : (↑q : ℝ) = HMul.hMul (α := ℝ) (↑y : ℝ) (↑y : ℝ)
mp₁ : (↑q : ℝ) = √(↑q : ℝ) * √(↑q : ℝ)
mp₂ mp₃ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
⊢ Eq (α := ℝ) (↑q : ℝ) (↑(y * y) : ℝ)

Tactic:
rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]

Premises used: Iff.mpr, Rat.cast_mul, Real.mul_self_sqrt, Rat.cast_nonneg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q' : ℚ
hq : 0 ≤ q' * q'
⊢ ∃ (y : ℚ), (↑y : ℝ) = √(↑(q' * q') : ℝ)

Tactic:
⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩

Premises used: abs, congrArg, cast, Rat.cast, Rat.cast_mul._simp_1, Real.sqrt_mul_self_eq_abs, congr, Exists.intro, Real.sqrt, Eq.symm, Eq, Rat.cast_abs._simp_1
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q' : ℚ
hq : 0 ≤ q' * q'
⊢ ∃ (y : ℚ), (↑y : ℝ) = √(↑(q' * q') : ℝ)

Tactic:
exact ⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
inl : ∀ (hq : 0 ≤ q), Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
inr : ∀ (hq : q < 0), Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
obtain hq | hq := le_or_gt 0 q

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : 0 ≤ q
inl : ¬IsSquare q ↔ ¬IsSquare q ∧ 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
simp_rw [irrational_sqrt_ratCast_iff_of_nonneg hq, and_iff_left hq]

Premises used: and_iff_left, irrational_sqrt_ratCast_iff_of_nonneg
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
hq : q < 0
inr : Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q
⊢ Irrational √(↑q : ℝ) ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
rw [sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 hq.le)]

Premises used: Iff.mpr, Real.sqrt_eq_zero_of_nonpos, LT.lt.le, Rat.cast_nonpos
-- Module: Mathlib.NumberTheory.Real.Irrational
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
inr₄ : ¬IsSquare q → True
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]

Premises used: not_le, not_irrational_zero, false_iff, implies_true, not_and
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
z : ℤ
hz : 0 ≤ z
rw : Irrational √(↑z : ℝ) ↔ ¬IsSquare (α := ℚ) (↑z : ℚ)
rw₁ : Irrational √(↑z : ℝ) ↔ Irrational √(↑(↑z : ℚ) : ℝ)
rw₂ rw₃ : Irrational √(↑z : ℝ) ↔ Irrational √(↑z : ℝ)
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z

Tactic:
rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz),
    Rat.cast_intCast]

Premises used: Rat.isSquare_intCast_iff, Rat.cast_intCast, irrational_sqrt_ratCast_iff_of_nonneg
-- Module: Mathlib.NumberTheory.Real.Irrational
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
rw₃ rw₄ : ¬IsSquare z ∧ 0 ≤ z ↔ ¬IsSquare z ∧ 0 ≤ z
⊢ Irrational √(↑z : ℝ) ↔ ¬IsSquare z ∧ 0 ≤ z

Tactic:
rw [← Rat.cast_intCast, irrational_sqrt_ratCast_iff, Rat.isSquare_intCast_iff,
    Int.cast_nonneg_iff]

Premises used: Rat.isSquare_intCast_iff, Rat.cast_intCast, irrational_sqrt_ratCast_iff, Int.cast_nonneg_iff
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
rw : Irrational √(↑n : ℝ) ↔ ¬IsSquare (α := ℚ) (↑n : ℚ)
rw₁ : Irrational √(↑n : ℝ) ↔ Irrational √(↑(↑n : ℚ) : ℝ)
rw₂ rw₃ : Irrational √(↑n : ℝ) ↔ Irrational √(↑n : ℝ)
⊢ Irrational √(↑n : ℝ) ↔ ¬IsSquare n

Tactic:
rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
    Rat.cast_natCast]

Premises used: Nat.cast_nonneg, irrational_sqrt_ratCast_iff_of_nonneg, Rat.isSquare_natCast_iff, Rat.cast_natCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Irrational √(OfNat.ofNat n) ↔ ¬IsSquare (α := ℕ) (OfNat.ofNat n)

Tactic:
irrational_sqrt_natCast_iff

Premises used: irrational_sqrt_natCast_iff
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
p : ℕ
hp : Prime p
⊢ Irrational √(↑p : ℝ)

Tactic:
irrational_sqrt_natCast_iff.mpr hp.not_isSquare

Premises used: Iff.mpr, Irreducible.not_isSquare, irrational_sqrt_natCast_iff
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
⊢ Irrational √2

Tactic:
simpa using Nat.prime_two.irrational_sqrt

Premises used: Nat.prime_two, Nat.Prime.irrational_sqrt
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
q : ℚ
⊢ x ≠ (↑q : ℝ)

Tactic:
fun hq => h ⟨q, hq.symm⟩

Premises used: Exists.intro, Eq.symm, Not
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ (↑(↑m : ℚ) : ℝ)

Tactic:
h.ne_rat _

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

Tactic:
exact h.ne_rat _

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

Tactic:
h.ne_int m

Premises used: Nat.cast, Irrational.ne_int
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
⊢ x ≠ 0

Tactic:
mod_cast h.ne_nat 0

Premises used: Irrational.ne_nat, congrArg, cast, Ne, Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
⊢ x ≠ 1

Tactic:
simpa only [Nat.cast_one] using h.ne_nat 1

Premises used: Irrational.ne_nat, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
n : ℕ
inst : n.AtLeastTwo
⊢ x ≠ OfNat.ofNat n

Tactic:
h.ne_nat n

Premises used: Irrational.ne_nat
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
⊢ ¬Irrational (↑q : ℝ)

Tactic:
fun h => h ⟨q, rfl⟩

Premises used: Exists.intro, Not, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
⊢ ¬Irrational (↑m : ℝ)

Tactic:
fun h => h.ne_int m rfl

Premises used: Irrational.ne_int, Not, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℕ
⊢ ¬Irrational (↑m : ℝ)

Tactic:
fun h => h.ne_nat m rfl

Premises used: Irrational.ne_nat, Not, rfl
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ¬Irrational (OfNat.ofNat n)

Tactic:
n.not_irrational

Premises used: Nat.not_irrational
-- 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) (HAdd.hAdd (α := ℝ) (↑rx : ℝ) (↑ry : ℝ))

Tactic:
⟨rx + ry, cast_add rx ry⟩

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

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

Tactic:
h.add_cases.resolve_left q.not_irrational

Premises used: Irrational.add_cases, Or.resolve_left, Rat.not_irrational
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational x
rwa : Irrational (-(↑q : ℝ) + ((↑q : ℝ) + x))
rwa₁ rwa₂ rwa₃ rwa₄ : Irrational x
⊢ Irrational ((↑(-q) : ℝ) + ((↑q : ℝ) + x))

Tactic:
rwa [cast_neg, neg_add_cancel_left]

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

Tactic:
add_comm (↑q) x ▸ of_ratCast_add q

Premises used: Eq.rec, add_comm, Irrational.of_ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x + (↑q : ℝ))

Tactic:
add_comm (↑q) x ▸ h.ratCast_add q

Premises used: Eq.rec, add_comm, Irrational.ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑m : ℝ) + x)
⊢ Irrational ((↑(↑m : ℚ) : ℝ) + x)

Tactic:
rw [← cast_intCast] at h

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

Tactic:
h.of_ratCast_add m

Premises used: Int.cast, Irrational.of_ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
m : ℤ
h : Irrational ((↑(↑m : ℚ) : ℝ) + x)
⊢ Irrational x

Tactic:
exact h.of_ratCast_add m

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

Tactic:
of_intCast_add m <| add_comm x m ▸ h

Premises used: Int.cast, Eq.rec, add_comm, Irrational.of_intCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational ((↑(↑m : ℚ) : ℝ) + x)

Tactic:
h.ratCast_add m

Premises used: Int.cast, Irrational.ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational ((↑(↑m : ℚ) : ℝ) + x)

Tactic:
exact h.ratCast_add m

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

Tactic:
add_comm (↑m) x ▸ h.intCast_add m

Premises used: Irrational.intCast_add, Eq.rec, add_comm