awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
hx' : x' = (↑x : ℤ)
⊢ a ≠ x ^ d

Tactic:
specialize ha x
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d

Tactic:
simp only [Int.cast_natCast, div_pow] at h

Premises used: Int.cast_natCast, div_pow
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
neg : ∀ (h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)), False
neg₁ : Ne (α := ℚ) (↑b : ℚ) 0
neg₂ : HPow.hPow (α := ℚ) (↑y : ℚ) d ≠ 0
⊢ False

Tactic:
rw [div_eq_div_iff] at h

Premises used: div_eq_div_iff
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
⊢ Ne (α := ℚ) (↑b : ℚ) 0

Tactic:
simpa
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
⊢ HPow.hPow (α := ℚ) (↑y : ℚ) d ≠ 0

Tactic:
simp [y]
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)
qify : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)
⊢ a * y ^ d = x ^ d * b

Tactic:
qify
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)
⊢ (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)

Tactic:
assumption
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)
⊢ a * y ^ d = x ^ d * b

Tactic:
replace h : a * y ^ d = x ^ d * b := by
    qify
    assumption
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
neg : a = x ^ d
⊢ False

Tactic:
apply ha
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
rhs : x ^ d * b
| a * y ^ d = x ^ d * b

Tactic:
rhs
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
rw : b * x ^ d
| x ^ d * b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
rw : b * x ^ d
| a * y ^ d = x ^ d * b

Tactic:
rhs; rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
⊢ a * y ^ d = b * x ^ d

Tactic:
conv at h => rhs; rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
apply : (y ^ d).Coprime (x ^ d)
⊢ a = x ^ d

Tactic:
apply eq_of_mul_eq_mul_of_coprime h_coprime _ h

Premises used: _private.0.Tactic.NormNum.eq_of_mul_eq_mul_of_coprime
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
H1 : y.Coprime (x ^ d)
⊢ (y ^ d).Coprime (x ^ d)

Tactic:
apply Nat.Coprime.pow_left

Premises used: Nat.Coprime.pow_left
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
H1 : y.Coprime x
⊢ y.Coprime (x ^ d)

Tactic:
apply Nat.Coprime.pow_right

Premises used: Nat.Coprime.pow_right
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
H1 : x.Coprime y
⊢ y.Coprime x

Tactic:
apply Nat.Coprime.symm

Premises used: Nat.Coprime.symm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
⊢ x.Coprime y

Tactic:
simpa [hx'] using (show x'.natAbs.Coprime y from Rat.reduced q)

Premises used: Rat.reduced
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
pos : ∀ (hq : 0 ≤ q), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
neg : ∀ (hq : ¬0 ≤ q), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
by_cases hq : 0 ≤ q
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
apply not_power_rat_of_num_aux h_coprime ha hq

Premises used: _private.0.Tactic.NormNum.not_power_rat_of_num_aux
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
neg : ∀ (h_even : Even d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
neg₁ : ∀ (h_odd : Odd d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
rcases d.even_or_odd with (h_even | h_odd)

Premises used: Nat.even_or_odd
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
linarith : -q < 0 → q - 0 + (-q - 0) = 0
⊢ 0 ≤ -q

Tactic:
linarith
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ (-q) ^ d

Tactic:
have := not_power_rat_of_num_aux h_coprime (q := -q) ha (by linarith)
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
this : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ (-q) ^ d
neg neg₁ neg₂ neg₃ :
  ∀ (this : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
rwa [h_even.neg_pow] at this

Premises used: Even.neg_pow
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
neg : ∀ (hq : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d), 0 ≤ q
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
contrapose hq
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d
neg : 0 ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)
⊢ 0 ≤ q

Tactic:
rw [← h_odd.pow_nonneg_iff, ← hq]

Premises used: Odd.pow_nonneg_iff
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
positivity
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
by_contra! : ∀ (h : y_den ≤ 0), False
⊢ 0 < y_den

Tactic:
by_contra! h
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den ≤ 0
⊢ y_den = 0

Tactic:
simp only [nonpos_iff_eq_zero] at h

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den = 0
⊢ 1 < x_num

Tactic:
simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2

Premises used: pow_zero, Nat.lt_one_iff
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den = 0
hn1₁ : 1 < x_num
⊢ x_num = 0

Tactic:
simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2

Premises used: pow_zero, Nat.lt_one_iff
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
h : y_den = 0
hn1 : 1 < x_num
hn2 : x_num = 0
⊢ False

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
⊢ 0 < y_den

Tactic:
have hy_den_pos : 0 < y_den := by
    by_contra! h
    simp only [nonpos_iff_eq_zero] at h
    simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2
    lia
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
rcases :
  ∀ (hx_inv : Invertible (α := ℝ) (↑x_den : ℝ))
    (hx_eq :
      x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)),
    Irrational (x ^ y)
⊢ Irrational (x ^ y)

Tactic:
rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
rcases :
  ∀ (hy_inv : Invertible (α := ℝ) (↑y_den : ℝ))
    (hy_eq :
      y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)),
    Irrational (x ^ y)
⊢ Irrational (x ^ y)

Tactic:
rcases hy_isNNRat with ⟨hy_inv, hy_eq⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
rw :
  Irrational
    (HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) ^
      HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _))
⊢ Irrational (x ^ y)

Tactic:
rw [hy_eq, hx_eq]
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
simp : HMul.hMul (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)
⊢ HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
⊢ HMul.hMul (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)

Tactic:
rfl
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
⊢ HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)

Tactic:
have h1 : (y_num * ⅟(y_den : ℝ) : ℝ) = ((y_num / y_den : ℚ) : ℝ) := by
    simp
    rfl
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
simp : HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)
⊢ HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)

Tactic:
rfl
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)

Tactic:
have h2 : (x_num * ⅟(x_den : ℝ) : ℝ) = ((x_num / x_den : ℚ) : ℝ) := by
    simp
    rfl
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
h2 :
  HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
rw :
  Irrational
    (HPow.hPow (α := ℝ) (β := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
      (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ))
⊢ Irrational
    (HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) ^
      HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _))

Tactic:
rw [h1, h2]
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
h2 :
  HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
⊢ Irrational
    (HPow.hPow (α := ℝ) (β := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
      (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ))

Tactic:
irrational_rpow_rat_of_not_power ?_ hy_den_pos ?_

Premises used: _private.0.Tactic.NormNum.irrational_rpow_rat_of_not_power
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
h2 :
  HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
refine_1 : ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ) ^ y_num ≠ p ^ y_den
refine_2 : 0 ≤ HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)
⊢ Irrational
    (HPow.hPow (α := ℝ) (β := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
      (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ))

Tactic:
refine irrational_rpow_rat_of_not_power ?_ hy_den_pos ?_

Premises used: _private.0.Tactic.NormNum.irrational_rpow_rat_of_not_power
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
hy_inv : Invertible (α := ℝ) (↑y_den : ℝ)
hy_eq : y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)
h1 :
  HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ)
h2 :
  HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) =
    (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
refine_1 : ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑(x_num ^ y_num) : ℚ) (↑(x_den ^ y_num) : ℚ) ≠ p ^ y_den
⊢ ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ) ^ y_num ≠ p ^ y_den

Tactic:
simp only [div_pow, ← Nat.cast_pow]

Premises used: div_pow, Nat.cast_pow