awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (x_num ^ y_num).Coprime (x_den ^ y_num)
refine_1₁ : ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den
⊢ ∀ (p : ℚ), HDiv.hDiv (α := ℚ) (↑(x_num ^ y_num) : ℚ) (↑(x_den ^ y_num) : ℚ) ≠ p ^ y_den

Tactic:
apply not_power_rat_of_num

Premises used: _private.0.Tactic.NormNum.not_power_rat_of_num
-- 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 : ℚ)) : ℝ)
⊢ (x_num ^ y_num).Coprime (x_den ^ y_num)

Tactic:
apply Nat.Coprime.pow _ _ hx_coprime

Premises used: Nat.Coprime.pow
-- 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 : ℚ)) : ℝ)
⊢ ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den

Tactic:
apply not_power_nat_pow_of_bounds hy_den_pos hy_coprime hn1 hn2

Premises used: _private.0.Tactic.NormNum.not_power_nat_pow_of_bounds
-- 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 : ℚ)) : ℝ)
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑x_num : ℚ) (↑x_den : ℚ)

Tactic:
positivity
-- Module: Mathlib.Tactic.NormNum.Irrational
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
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_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 : ℝ) _)
h : Irrational (x ^ y)⁻¹
⊢ Irrational (x ^ y)

Tactic:
apply Irrational.of_inv

Premises used: Irrational.of_inv
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
simp : 0 ≤ HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹
⊢ 0 ≤ x

Tactic:
simp only [hx_eq, invOf_eq_inv]

Premises used: invOf_eq_inv
-- Module: Mathlib.Tactic.NormNum.Irrational
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 ≤ HMul.hMul (α := ℝ) (↑x_num : ℝ) (↑x_den : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
h : Irrational (x⁻¹ ^ y)
⊢ Irrational (x ^ y)⁻¹

Tactic:
rw [← Real.inv_rpow (by simp only [hx_eq, invOf_eq_inv]; positivity)]

Premises used: Real.inv_rpow
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
apply : IsNNRat x⁻¹ x_den x_num
⊢ Irrational (x⁻¹ ^ y)

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

Premises used: Tactic.NormNum.irrational_rpow_rat_rat_of_num, Nat.coprime_comm, Iff.mp
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
⊢ x⁻¹ = HMul.hMul (α := ℝ) (↑x_den : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_num : ℝ) _)

Tactic:
simp [hx_eq]
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
refine : Eq (α := ℝ) (↑x_num : ℝ) 0 → False
⊢ IsNNRat x⁻¹ x_den x_num

Tactic:
refine ⟨invertibleOfNonzero (fun _ ↦ ?_), by simp [hx_eq]⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ) _)
h : Eq (α := ℝ) (↑x_num : ℝ) 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x y : ℝ
x_num y_num y_den k : ℕ
hx_isNat : IsNat x x_num
hy_isNNRat : IsNNRat y y_num y_den
hy_coprime : y_num.Coprime y_den
hn1 : k ^ y_den < x_num
hn2 : x_num < (k + 1) ^ y_den
⊢ x_num.Coprime 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
rw : Irrational (x ^ (1 / 2))
⊢ Irrational √x

Tactic:
rw [Real.sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ Nat.Coprime 1 2

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
apply : IsNNRat (1 / 2) 1 2
⊢ Irrational (x ^ (1 / 2))

Tactic:
apply irrational_rpow_rat_rat_of_num hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hn1 hn2

Premises used: Tactic.NormNum.irrational_rpow_rat_rat_of_num
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ 1 / 2 * (↑2 : ℝ) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ (↑2 : ℝ) * (1 / 2) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ 1 / 2 = HMul.hMul (α := ℝ) (↑1 : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑2 : ℝ) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ IsNNRat (1 / 2) 1 2

Tactic:
exact ⟨Invertible.mk (1/2) (by simp) (by simp), by simp⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
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
rw : Irrational (x ^ (1 / 2))
⊢ Irrational √x

Tactic:
rw [Real.sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ Nat.Coprime 1 2

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
apply : IsNNRat (1 / 2) 1 2
⊢ Irrational (x ^ (1 / 2))

Tactic:
apply irrational_rpow_rat_rat_of_den hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hd1 hd2

Premises used: Tactic.NormNum.irrational_rpow_rat_rat_of_den
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ 1 / 2 * (↑2 : ℝ) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ (↑2 : ℝ) * (1 / 2) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ 1 / 2 = HMul.hMul (α := ℝ) (↑1 : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑2 : ℝ) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ IsNNRat (1 / 2) 1 2

Tactic:
exact ⟨Invertible.mk (1/2) (by simp) (by simp), by simp⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
x : ℝ
n k : ℕ
hx_isNat : IsNat x n
hn1 : HPow.hPow (β := ℕ) k 2 < n
hn2 : n < HPow.hPow (β := ℕ) (k + 1) 2
⊢ n.Coprime 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.IsCoprime
Goal:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
rw : ¬d = 1
⊢ ¬IsCoprime x y

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, hd]

Premises used: Int.isCoprime_iff_gcd_eq_one
-- Module: Mathlib.Tactic.NormNum.IsCoprime
Goal:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1

Tactic:
Nat.ne_of_beq_eq_false h

Premises used: Nat.ne_of_beq_eq_false
-- Module: Mathlib.Tactic.NormNum.IsCoprime
Goal:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1

Tactic:
exact Nat.ne_of_beq_eq_false h

Premises used: Nat.ne_of_beq_eq_false
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a n : ℕ
h : IsNat a n
m : ℕ
hm : m * m = n
⊢ IsSquare a

Tactic:
⟨m, h.1.trans hm.symm⟩

Premises used: IsSquare, Exists.intro, Mathlib.Meta.NormNum.IsNat.out, Eq.symm, Eq.trans
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
⊢ k.blt a = true

Tactic:
rcases h with ⟨rfl⟩

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
⊢ a.ble (k + 2 * m) = true

Tactic:
rcases h with ⟨rfl⟩

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a m k : ℕ
hm : m * m = k
hk₁ : k.blt a = true
hk₂ : a.ble (k + 2 * m) = true
⊢ (m * m).blt a = true

Tactic:
subst k
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
⊢ a.ble (m * m + 2 * m) = true

Tactic:
subst k
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
m b : ℕ
hk₁ : (m * m).blt (b * b) = true
hk₂ : (b * b).ble (m * m + 2 * m) = true
⊢ m < b

Tactic:
simp only [Nat.blt_eq, Nat.ble_eq, ← sq, Nat.pow_lt_pow_iff_left two_ne_zero] at hk₁ hk₂

Premises used: Nat.ble_eq, sq, Nat.pow_lt_pow_iff_left, two_ne_zero, Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
m b : ℕ
hk₁ : (m * m).blt (b * b) = true
hk₂ : (b * b).ble (m * m + 2 * m) = true
hk₃ : m < b
⊢ 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₂

Premises used: Nat.ble_eq, sq, Nat.pow_lt_pow_iff_left, two_ne_zero, Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
m b : ℕ
hk₁ : m < b
hk₂ : HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m
⊢ 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₁

Premises used: Nat.pow_le_pow_iff_left, two_ne_zero, Nat.add_one_le_iff
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
m b : ℕ
hk₁ : m < b
hk₂ : HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m
hk₃ : HPow.hPow (β := ℕ) (m + 1) 2 ≤ HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m

Tactic:
rw [← Nat.add_one_le_iff, ← Nat.pow_le_pow_iff_left two_ne_zero] at hk₁

Premises used: Nat.pow_le_pow_iff_left, two_ne_zero, Nat.add_one_le_iff
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
m b : ℕ
hk₁ : HPow.hPow (β := ℕ) (m + 1) 2 ≤ HPow.hPow (β := ℕ) b 2
hk₂ : HPow.hPow (β := ℕ) b 2 ≤ HPow.hPow (β := ℕ) m 2 + 2 * m
⊢ False

Tactic:
grind
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
simp [h.1, Int.isSquare_natCast_iff]

Premises used: Mathlib.Meta.NormNum.IsNat.out, Int.isSquare_natCast_iff
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
simp [h.1, h']

Premises used: Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
refine : IsSquare a → ∀ (b : ℤ) (hb : a = b * b), n = 0
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : a = b * b
⊢ -(↑n : ℤ) = b * b

Tactic:
rw [h.1, Int.cast_negOfNat] at hb

Premises used: Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
inr : ∀ (hb₀ : b ≠ 0), n = 0
⊢ n = 0

Tactic:
rcases eq_or_ne b 0 with rfl | hb₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
hb : -(↑n : ℤ) = HMul.hMul (α := ℤ) 0 0
⊢ n = 0

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
absurd hb (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
hb₀ : b ≠ 0
inr : -(↑n : ℤ) < b * b
⊢ n = 0

Tactic:
refine absurd hb (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
hb₀ : b ≠ 0
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℤ
hb : -(↑n : ℤ) = b * b
hb₀ : b ≠ 0
⊢ -(↑n : ℤ) < b * b

Tactic:
exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

Premises used: Iff.mpr, lt_of_le_of_lt, mul_self_pos
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
simp [h.1]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
simp [h.1, h']

Premises used: Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
refine : IsSquare a → ∀ (b : ℚ) (hb : a = b * b), n = 0
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : a = b * b
⊢ -(↑n : ℚ) = b * b

Tactic:
rw [h.1, Int.cast_negOfNat] at hb

Premises used: Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
inr : ∀ (hb₀ : b ≠ 0), n = 0
⊢ n = 0

Tactic:
rcases eq_or_ne b 0 with rfl | hb₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
hb : -(↑n : ℚ) = HMul.hMul (α := ℚ) 0 0
⊢ n = 0

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
absurd hb (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
hb₀ : b ≠ 0
inr : -(↑n : ℚ) < b * b
⊢ n = 0

Tactic:
refine absurd hb (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
hb₀ : b ≠ 0
⊢ LE.le (α := ℚ) (-(↑n : ℚ)) 0

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h_1 : IsSquare a
b : ℚ
hb : -(↑n : ℚ) = b * b
hb₀ : b ≠ 0
⊢ -(↑n : ℚ) < b * b

Tactic:
exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

Premises used: Iff.mpr, lt_of_le_of_lt, mul_self_pos
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : IsSquare n
hd : IsSquare d
ha : IsNNRat a n d
rcases : ∀ (n : ℕ) (ha : IsNNRat a (n * n) d), IsSquare a
⊢ IsSquare a

Tactic:
rcases hn with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
d : ℕ
hd : IsSquare d
n : ℕ
ha : IsNNRat a (n * n) d
rcases : ∀ (d : ℕ) (ha : IsNNRat a (n * n) (d * d)), IsSquare a
⊢ IsSquare a

Tactic:
rcases hd with ⟨d, rfl⟩

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
ha : IsNNRat a (n * n) (d * d)
h : a = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) * HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ IsSquare a

Tactic:
use n / d
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
ha : IsNNRat a (n * n) (d * d)
⊢ a = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) * HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)

Tactic:
simp [ha.to_eq, div_mul_div_comm]

Premises used: div_mul_div_comm, Mathlib.Meta.NormNum.IsNNRat.to_eq
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
rw : ¬(IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).den)
hb0 : LT.lt (α := ℤ) 0 (↑d : ℤ)
h : (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))
⊢ ¬IsSquare a

Tactic:
rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    Rat.num_div_eq_of_coprime]

Premises used: Int.cast_natCast, Mathlib.Meta.NormNum.IsNNRat.to_eq, Rat.isSquare_iff, Rat.num_div_eq_of_coprime, rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).den)

Tactic:
simp [hn]
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
hb0 : ∀ (hnd : LE.le (α := ℤ) (↑d : ℤ) 0), n.gcd d ≠ 1
⊢ LT.lt (α := ℤ) 0 (↑d : ℤ)

Tactic:
contrapose! hnd
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
d : ℕ
hnd : LE.le (α := ℤ) (↑d : ℤ) 0
hn : ¬IsSquare (α := ℕ) 1
ha : IsNNRat a 1 d
⊢ False

Tactic:
simp at hn
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : LE.le (α := ℤ) (↑d : ℤ) 0
⊢ n ≠ 1

Tactic:
have : n ≠ 1 := by rintro rfl; simp at hn