awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℝ) _)
⊢ Irrational (x ^ y)
have rcases : ∀ (hy_inv : Invertible (α := ℝ) (↑y_den : ℝ))
  (hy_eq :
    y = HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _)),
  Irrational (x ^ y)
Tactic: rcases hy_isNNRat with ⟨hy_inv, hy_eq⟩
Cleared hypotheses: hy_isNNRat
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℝ) _)
⊢ Irrational (x ^ y)
have 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 : ℝ) _))
Tactic: rw [hy_eq, hx_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℚ)) : ℝ)
have simp : HMul.hMul (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑y_num : ℝ) (↑y_den : ℝ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
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 : ℝ) _)
⊢ 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 : ℝ) _))
have h1 : 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
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℚ)) : ℝ)
have simp : HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹ = HDiv.hDiv (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
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 : ℚ)) : ℝ)
⊢ 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 : ℝ) _))
have h2 : 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
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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
    (HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _) ^
      HMul.hMul (α := ℝ) (↑y_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑y_den : ℝ) _))
have rw : Irrational
  (HPow.hPow (α := ℝ) (β := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
    (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ))
Tactic: rw [h1, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℚ)) : ℝ))
have refine_1 : ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ) ^ y_num ≠ p ^ y_den
Tactic: refine irrational_rpow_rat_of_not_power ?_ hy_den_pos ?_
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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
⊢ Irrational
    (HPow.hPow (α := ℝ) (β := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)) : ℝ)
      (↑(HDiv.hDiv (α := ℚ) (↑y_num : ℚ) (↑y_den : ℚ)) : ℝ))
have refine_2 : 0 ≤ HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)
Tactic: refine irrational_rpow_rat_of_not_power ?_ hy_den_pos ?_
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℚ)) : ℝ)
⊢ ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ) ^ y_num ≠ p ^ y_den
have refine_1 : ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑(x_num ^ y_num) : ℚ) (↑(x_den ^ y_num) : ℚ) ≠ p ^ y_den
Tactic: simp only [div_pow, ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : ℚ)) : ℝ)
⊢ ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑(x_num ^ y_num) : ℚ) (↑(x_den ^ y_num) : ℚ) ≠ p ^ y_den
have refine_1 : (x_num ^ y_num).Coprime (x_den ^ y_num)
Tactic: apply not_power_rat_of_num
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
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 : (x_num ^ y_num).Coprime (x_den ^ y_num)
⊢ ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑(x_num ^ y_num) : ℚ) (↑(x_den ^ y_num) : ℚ) ≠ p ^ y_den
have refine_1₁ : ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den
Tactic: apply not_power_rat_of_num
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
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
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
⊢ Irrational (x ^ y)
have rcases : ∀ (hx_inv : Invertible (α := ℝ) (↑x_den : ℝ))
  (hx_eq :
    x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)),
  Irrational (x ^ y)
Tactic: rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩
Cleared hypotheses: hx_isNNRat
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
⊢ Irrational (x ^ y)
have h : Irrational (x ^ y)⁻¹
Tactic: apply Irrational.of_inv
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
⊢ 0 ≤ x
have simp : 0 ≤ HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹
Tactic: simp only [hx_eq, invOf_eq_inv]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
⊢ Irrational (x ^ y)⁻¹
have h : Irrational (x⁻¹ ^ y)
Tactic: rw [← Real.inv_rpow (by simp only [hx_eq, invOf_eq_inv]; positivity)]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
⊢ Irrational (x⁻¹ ^ y)
have apply : IsNNRat x⁻¹ x_den x_num
Tactic: apply irrational_rpow_rat_rat_of_num (x_num := x_den) (x_den := x_num) _ hy_isNNRat
    (Nat.coprime_comm.mp hx_coprime) hy_coprime hd1 hd2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible (α := ℝ) (↑x_den : ℝ)
hx_eq : x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)
⊢ IsNNRat x⁻¹ x_den x_num
have refine : Eq (α := ℝ) (↑x_num : ℝ) 0 → False
Tactic: refine ⟨invertibleOfNonzero (fun _ ↦ ?_), by simp [hx_eq]⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : HPow.hPow (β := ℕ) num_k 2 < num
hn2 : num < HPow.hPow (β := ℕ) (num_k + 1) 2
⊢ Irrational √x
have rw : Irrational (x ^ (1 / 2))
Tactic: rw [Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : HPow.hPow (β := ℕ) num_k 2 < num
hn2 : num < HPow.hPow (β := ℕ) (num_k + 1) 2
⊢ Irrational (x ^ (1 / 2))
have apply : IsNNRat (1 / 2) 1 2
Tactic: apply irrational_rpow_rat_rat_of_num hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hn1 hn2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : HPow.hPow (β := ℕ) den_k 2 < den
hd2 : den < HPow.hPow (β := ℕ) (den_k + 1) 2
⊢ Irrational √x
have rw : Irrational (x ^ (1 / 2))
Tactic: rw [Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : HPow.hPow (β := ℕ) den_k 2 < den
hd2 : den < HPow.hPow (β := ℕ) (den_k + 1) 2
⊢ Irrational (x ^ (1 / 2))
have apply : IsNNRat (1 / 2) 1 2
Tactic: apply irrational_rpow_rat_rat_of_den hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hd1 hd2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsCoprime (goal)
Goal:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬IsCoprime x y
have rw : ¬d = 1
Tactic: rw [Int.isCoprime_iff_gcd_eq_one, hd]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a n : ℕ
h : IsNat a n
m k : ℕ
hm : m * m = k
hk₁ : k.blt n = true
hk₂ : n.ble (k + 2 * m) = true
⊢ ¬IsSquare a
have hk₃ : k.blt a = true
Tactic: rcases h with ⟨rfl⟩
Cleared hypotheses: n, h, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a n : ℕ
h : IsNat a n
m k : ℕ
hm : m * m = k
hk₁ : k.blt n = true
hk₂ : n.ble (k + 2 * m) = true
hk₃ : k.blt a = true
⊢ ¬IsSquare a
have hk₄ : a.ble (k + 2 * m) = true
Tactic: rcases h with ⟨rfl⟩
Cleared hypotheses: n, h, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a m k : ℕ
hm : m * m = k
hk₁ : k.blt a = true
hk₂ : a.ble (k + 2 * m) = true
⊢ ¬IsSquare a
have hk₃ : (m * m).blt a = true
Tactic: subst k
Cleared hypotheses: k, hm, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a m k : ℕ
hm : m * m = k
hk₁ : k.blt a = true
hk₂ : a.ble (k + 2 * m) = true
hk₃ : (m * m).blt a = true
⊢ ¬IsSquare a
have hk₄ : a.ble (m * m + 2 * m) = true
Tactic: subst k
Cleared hypotheses: k, hm, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
m b : ℕ
hk₁ : (m * m).blt (b * b) = true
hk₂ : (b * b).ble (m * m + 2 * m) = true
⊢ False
have hk₃ : m < b
Tactic: simp only [Nat.blt_eq, Nat.ble_eq, ← sq, Nat.pow_lt_pow_iff_left two_ne_zero] at hk₁ hk₂
Cleared hypotheses: hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
m b : ℕ
hk₁ : (m * m).blt (b * b) = true
hk₂ : (b * b).ble (m * m + 2 * m) = true
hk₃ : m < b
⊢ False
have hk₄ : HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m
Tactic: simp only [Nat.blt_eq, Nat.ble_eq, ← sq, Nat.pow_lt_pow_iff_left two_ne_zero] at hk₁ hk₂
Cleared hypotheses: hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
m b : ℕ
hk₁ : m < b
hk₂ : HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m
⊢ False
have hk₃ : HPow.hPow (β := ℕ) (m + 1) 2 ≤ HPow.hPow (β := ℕ) b 2
Tactic: rw [← Nat.add_one_le_iff, ← Nat.pow_le_pow_iff_left two_ne_zero] at hk₁
Cleared hypotheses: hk₁, hk₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a
have refine : IsSquare a → ∀ (b : ℤ) (hb : a = b * b), n = 0
Tactic: refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : a = b * b
⊢ n = 0
have hb₁ : -(↑n : ℤ) = b * b
Tactic: rw [h.1, Int.cast_negOfNat] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
⊢ n = 0
have inl : ∀ (hb : -(↑n : ℤ) = HMul.hMul (α := ℤ) 0 0), n = 0
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
inl : ∀ (hb : -(↑n : ℤ) = HMul.hMul (α := ℤ) 0 0), n = 0
⊢ n = 0
have inr : ∀ (hb₀ : b ≠ 0), n = 0
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
hb₀ : b ≠ 0
⊢ n = 0
have inr : -(↑n : ℤ) < b * b
Tactic: refine absurd hb (ne_of_lt ?_)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a
have refine : IsSquare a → ∀ (b : ℚ) (hb : a = b * b), n = 0
Tactic: refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : a = b * b
⊢ n = 0
have hb₁ : -(↑n : ℚ) = b * b
Tactic: rw [h.1, Int.cast_negOfNat] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
⊢ n = 0
have inl : ∀ (hb : -(↑n : ℚ) = HMul.hMul (α := ℚ) 0 0), n = 0
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
inl : ∀ (hb : -(↑n : ℚ) = HMul.hMul (α := ℚ) 0 0), n = 0
⊢ n = 0
have inr : ∀ (hb₀ : b ≠ 0), n = 0
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
hb₀ : b ≠ 0
⊢ n = 0
have inr : -(↑n : ℚ) < b * b
Tactic: refine absurd hb (ne_of_lt ?_)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : IsSquare n
hd : IsSquare d
ha : IsNNRat a n d
⊢ IsSquare a
have rcases : ∀ (n : ℕ) (ha : IsNNRat a (n * n) d), IsSquare a
Tactic: rcases hn with ⟨n, rfl⟩
Cleared hypotheses: n, hn, ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
d : ℕ
hd : IsSquare d
n : ℕ
ha : IsNNRat a (n * n) d
⊢ IsSquare a
have rcases : ∀ (d : ℕ) (ha : IsNNRat a (n * n) (d * d)), IsSquare a
Tactic: rcases hd with ⟨d, rfl⟩
Cleared hypotheses: d, hd, ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
ha : IsNNRat a (n * n) (d * d)
⊢ IsSquare a
have h : a = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) * HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
Tactic: use n / d