awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
left : (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = c
left₁ : (HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)).num = c
left₂ left₃ : c = c
⊢ a = c

Tactic:
rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]

Premises used: Rat.num_div_eq_of_coprime
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
right : (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).den : ℤ) = d
right₁ : (↑(HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)).den : ℤ) = d
right₂ right₃ : d = d
⊢ b = d

Tactic:
rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]

Premises used: Rat.den_div_eq_of_coprime
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
pos : ∀ (hn : n = 0), (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
neg : ∀ (hn : ¬n = 0), (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
hn : n = 0
pos : (↑(0 / 0) : ℚ) = HDiv.hDiv (α := ℚ) (↑0 : ℚ) (↑0 : ℚ)
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)

Tactic:
subst hn
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
⊢ (↑(0 / 0) : ℚ) = HDiv.hDiv (α := ℚ) (↑0 : ℚ) (↑0 : ℚ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
hn : ¬n = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hn : ¬Eq (α := ℚ) (↑n : ℚ) (↑0 : ℚ)), Ne (α := ℚ) (↑n : ℚ) 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
rwa [← coe_int_inj] at hn

Premises used: Rat.coe_int_inj
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
hn : ¬n = 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
hn : ¬n = 0
this : Ne (α := ℚ) (↑n : ℚ) 0
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)

Tactic:
simp only [Int.ediv_self hn, Int.cast_one, div_self this]

Premises used: Int.ediv_self, div_self, Int.cast_one
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)

Tactic:
intCast_div_self n

Premises used: Rat.intCast_div_self, Nat.cast, Int.ediv
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
h : b ∣ a
rcases : ∀ (c : ℤ), (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
⊢ (↑(a / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
rcases h with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
b c : ℤ
rw : (↑(c * b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
rw₁ : (↑(c * (b / b)) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
rw₂ : HMul.hMul (α := ℚ) (↑c : ℚ) (↑(b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
rw₃ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
rw₄ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = HMul.hMul (α := ℚ) (↑c : ℚ) (↑b : ℚ) / (↑b : ℚ)
rw₅ rw₆ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)

Tactic:
rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
    intCast_div_self, Int.cast_mul, mul_div_assoc]

Premises used: mul_div_assoc, Int.mul_ediv_assoc, Rat.intCast_div_self, Int.cast_mul, mul_comm, dvd_refl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℕ
h : b ∣ a
⊢ (↑(a / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
intCast_div a b (Int.ofNat_dvd.mpr h)

Premises used: Iff.mpr, Int.ofNat_dvd, Nat.cast, Rat.intCast_div, Int.ediv
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : n ≠ 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
mp : (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 → n ∣ m
mpr : n ∣ m → (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 ↔ n ∣ m

Tactic:
constructor
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
mp : HMul.hMul (α := ℚ) (↑(HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).num : ℚ) (↑n : ℚ) = (↑m : ℚ) → n ∣ m
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 → n ∣ m

Tactic:
rw [Rat.den_eq_one_iff, eq_div_iff hn]

Premises used: Rat.den_eq_one_iff, eq_div_iff
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).num : ℚ) (↑n : ℚ) = (↑m : ℚ) → n ∣ m

Tactic:
mod_cast (Dvd.intro_left _)

Premises used: Int.cast, Rat.num, Dvd.dvd, congrArg, Rat.intCast_inj._simp_1, cast, HDiv.hDiv, Dvd.intro_left, Int.cast_mul._simp_1, implies_congr, Eq.refl, congrFun', Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).num : ℚ) (↑n : ℚ) = (↑m : ℚ) → n ∣ m

Tactic:
exact mod_cast (Dvd.intro_left _)

Premises used: Dvd.intro_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ n ∣ m → (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1

Tactic:
(intCast_div _ _ · ▸ rfl)

Premises used: Eq.rec, Rat.intCast_div, rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ n ∣ m → (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1

Tactic:
exact (intCast_div _ _ · ▸ rfl)
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 ↔ n ∣ m

Tactic:
(den_div_intCast_eq_one_iff m n (Int.ofNat_ne_zero.mpr hn)).trans Int.ofNat_dvd

Premises used: Iff.mpr, Int.ofNat_dvd, Nat.cast, Int.ofNat_ne_zero, Rat.den_div_intCast_eq_one_iff, Iff.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
ha0 : 0 < a
⊢ num (↑a : ℚ)⁻¹ = 1

Tactic:
simp [*]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
ha0 : 0 < a
⊢ num (↑a : ℚ)⁻¹ = 1

Tactic:
inv_intCast_num_of_pos (mod_cast ha0 : 0 < (a : ℤ))

Premises used: congrArg, Rat.inv_intCast_num_of_pos, cast, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Int.ofNat_lt._simp_1, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
ha0 : 0 < a
simp : (↑(if a = 0 then 1 else a.natAbs) : ℤ) = a
⊢ (↑(den (↑a : ℚ)⁻¹) : ℤ) = a

Tactic:
simp only [den_inv, num_intCast]

Premises used: Rat.num_intCast, Rat.den_inv
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
ha0 : 0 < a
⊢ (↑(if a = 0 then 1 else a.natAbs) : ℤ) = a

Tactic:
grind
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
ha0 : 0 < a
rw : LT.lt (α := ℤ) 0 (↑a : ℤ)
⊢ den (↑a : ℚ)⁻¹ = a

Tactic:
rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]

Premises used: Int.cast_natCast, Int.ofNat_inj, Rat.inv_intCast_den_of_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
ha0 rwa rwa₁ rwa₂ rwa₃ : 0 < a
⊢ LT.lt (α := ℤ) 0 (↑a : ℤ)

Tactic:
rwa [Int.natCast_pos]

Premises used: Int.natCast_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
⊢ num (↑a : ℚ)⁻¹ = a.sign

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
⊢ num (↑a : ℚ)⁻¹ = Int.sign (↑a : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ 2 ≤ a

Tactic:
have : 2 ≤ a := Nat.AtLeastTwo.prop
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
inst : a.AtLeastTwo
this : 2 ≤ a
simp : LT.lt (α := ℤ) 0 (OfNat.ofNat a)
⊢ num (OfNat.ofNat a)⁻¹ = 1

Tactic:
simp only [num_inv, num_ofNat, den_ofNat, Nat.cast_one, mul_one, Int.sign_eq_one_iff_pos,
    gt_iff_lt]

Premises used: Int.sign_eq_one_iff_pos, Rat.den_ofNat, Rat.num_inv, gt_iff_lt, mul_one, Rat.num_ofNat, Nat.cast_one
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
inst : a.AtLeastTwo
this : 2 ≤ a
⊢ LT.lt (α := ℤ) 0 (↑a : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
⊢ den (↑a : ℚ)⁻¹ = if a = 0 then 1 else a.natAbs

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
⊢ den (↑a : ℚ)⁻¹ = if a = 0 then 1 else a

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ den (OfNat.ofNat a)⁻¹ = OfNat.ofNat a

Tactic:
simp [den_inv, Int.natAbs_eq_iff]

Premises used: Int.natAbs_eq_iff, Rat.den_inv
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
hq : q ≠ 0
⊢ q⁻¹.den = q.num.natAbs

Tactic:
simp [*]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
p : ℚ → Prop
h : ∀ (a b : ℤ), b ≠ 0 → p (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ))
q : ℚ
⊢ p q

Tactic:
simpa [num_div_den] using h q.num q.den (mod_cast q.den_ne_zero)

Premises used: Rat.num_div_den, Rat.num, congrArg, Rat.den_ne_zero, cast, Rat.den, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
p : ℚ → Prop
⊢ (∃ (r : ℚ), p r) ↔ ∃ (a : ℤ), ∃ (b : ℤ), b ≠ 0 ∧ p (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ))

Tactic:
simpa using Rat.forall (p := (¬ p ·)).not

Premises used: Iff.not, Rat.forall
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
x : ℚ
⊢ (↑x.pnatDen : ℕ) = x.den

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
x : ℚ
n : ℕ+
⊢ x.pnatDen = n ↔ x.den = (↑n : ℕ)

Tactic:
Subtype.ext_iff

Premises used: PNat.val, Subtype.ext_iff, PNat
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
⊢ pnatDen 1 = 1

Tactic:
rfl

Premises used: Rat.pnatDen, rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
⊢ pnatDen 0 = 1

Tactic:
rfl

Premises used: Rat.pnatDen, rfl
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ)

Tactic:
positivity
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ 0 < HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2

Tactic:
positivity
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
rw :
  HPow.hPow (α := ℚ) (β := ℕ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 2 ≤
    (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ)) 2 ≤ (↑x : ℚ)

Tactic:
rw [div_pow, div_le_iff₀ (by positivity)]

Premises used: div_le_iff₀, div_pow
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
norm_cast : HPow.hPow (β := ℕ) (x * HPow.hPow (β := ℕ) prec 2).sqrt 2 ≤ x * HPow.hPow (β := ℕ) prec 2
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 2 ≤
    (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ HPow.hPow (β := ℕ) (x * HPow.hPow (β := ℕ) prec 2).sqrt 2 ≤ x * HPow.hPow (β := ℕ) prec 2

Tactic:
sqrt_le' (x * prec ^ 2)

Premises used: HMul.hMul, Nat.sqrt_le', HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ HPow.hPow (β := ℕ) (x * HPow.hPow (β := ℕ) prec 2).sqrt 2 ≤ x * HPow.hPow (β := ℕ) prec 2

Tactic:
exact sqrt_le' (x * prec ^ 2)

Premises used: HMul.hMul, Nat.sqrt_le', HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
rw :
  (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
        (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ))
        2 *
      HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2
⊢ (↑x : ℚ) <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2

Tactic:
rw [← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)]

Premises used: mul_lt_mul_iff_of_pos_right
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
rw :
  (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) * (↑prec : ℚ) +
        HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ) * (↑prec : ℚ))
      2
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
        (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ))
        2 *
      HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2

Tactic:
rw [← mul_pow, add_mul]

Premises used: add_mul, mul_pow
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
rw :
  (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 1) 2
h₁ h₂ : Ne (α := ℚ) (↑prec : ℚ) 0
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) * (↑prec : ℚ) +
        HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ) * (↑prec : ℚ))
      2

Tactic:
rw [div_mul_cancel₀, div_mul_cancel₀]

Premises used: div_mul_cancel₀
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
norm_cast : x * HPow.hPow (β := ℕ) prec 2 < HPow.hPow (β := ℕ) ((x * HPow.hPow (β := ℕ) prec 2).sqrt + 1) 2
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 1) 2

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ x * HPow.hPow (β := ℕ) prec 2 < HPow.hPow (β := ℕ) ((x * HPow.hPow (β := ℕ) prec 2).sqrt + 1) 2

Tactic:
lt_succ_sqrt' (x * prec ^ 2)

Premises used: HMul.hMul, HPow.hPow, Nat.lt_succ_sqrt', OfNat.ofNat
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ x * HPow.hPow (β := ℕ) prec 2 < HPow.hPow (β := ℕ) ((x * HPow.hPow (β := ℕ) prec 2).sqrt + 1) 2

Tactic:
exact lt_succ_sqrt' (x * prec ^ 2)

Premises used: HMul.hMul, HPow.hPow, Nat.lt_succ_sqrt', OfNat.ofNat
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
h₁ : ¬prec = 0
⊢ Ne (α := ℚ) (↑prec : ℚ) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Defs
Goal:
x prec : ℕ
h : 0 < prec
⊢ ¬prec = 0

Tactic:
positivity
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
⊢ HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)

Tactic:
have := ratSqrt_sq_le (x := x) h
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)

Tactic:
have : (x.ratSqrt prec ^ 2 : ℝ) ≤ ↑x := by norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
this : HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2) ≤ √(↑x : ℝ)

Tactic:
have := Real.sqrt_monotone this
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
this_2 : HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)
this : √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2) ≤ √(↑x : ℝ)
rwa : LE.le (α := ℝ) 0 (↑(x.ratSqrt prec) : ℝ)
⊢ (↑(x.ratSqrt prec) : ℝ) ≤ √(↑x : ℝ)

Tactic:
rwa [Real.sqrt_sq] at this

Premises used: Real.sqrt_sq
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
this_2 : HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)
this : √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2) ≤ √(↑x : ℝ)
⊢ LE.le (α := ℝ) 0 (↑(x.ratSqrt prec) : ℝ)

Tactic:
simpa only [Rat.cast_nonneg] using ratSqrt_nonneg _ _

Premises used: Nat.ratSqrt_nonneg, Rat.cast_nonneg
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2

Tactic:
have := lt_ratSqrt_add_inv_prec_sq (x := x) h
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
⊢ LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
⊢ LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)

Tactic:
have : (x : ℝ) < ↑((x.ratSqrt prec + 1 / prec) ^ 2 : ℚ) := by norm_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
⊢ LE.le (α := ℝ) 0 (↑x : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
⊢ √(↑x : ℝ) < √(↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)

Tactic:
have := Real.sqrt_lt_sqrt (by simp) this
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < √(↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
rw :
  ∀ (this : √(↑x : ℝ) < (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)),
    √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
rw₁ :
  ∀ (this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)),
    LE.le (α := ℝ) 0 (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
rw [Rat.cast_pow, Real.sqrt_sq] at this

Premises used: Real.sqrt_sq, Rat.cast_pow
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
push_cast at this
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
this
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
exact this
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)
push_cast : 0 ≤ (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
⊢ LE.le (α := ℝ) 0 (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)
⊢ LE.le (α := ℝ) 0 (↑(x.ratSqrt prec) : ℝ)

Tactic:
simpa using ratSqrt_nonneg _ _

Premises used: Nat.ratSqrt_nonneg
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
this_1 : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
this_2 : LT.lt (α := ℝ) (↑x : ℝ) (↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)
⊢ 0 ≤ (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)

Tactic:
exact add_nonneg (by simpa using ratSqrt_nonneg _ _) (by simp)

Premises used: add_nonneg
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
⊢ √(↑x : ℝ) ∈ Set.Ico (↑(x.ratSqrt prec) : ℝ) ((↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ))

Tactic:
grind [ratSqrt_le_realSqrt, realSqrt_lt_ratSqrt_add_inv_prec]

Premises used: Nat.realSqrt_lt_ratSqrt_add_inv_prec, Nat.ratSqrt_le_realSqrt
-- Module: Mathlib.Data.Rat.NatSqrt.Real
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑(x.ratSqrt prec) : ℝ) ∈ Set.Ioc (√(↑x : ℝ) - HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)) √(↑x : ℝ)

Tactic:
grind [ratSqrt_le_realSqrt]

Premises used: Nat.ratSqrt_le_realSqrt
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
q : ℚ
rw : mkRat (Int.sqrt (q * q).num) (q * q).den.sqrt = |q|
rw₁ : mkRat (Int.sqrt (q.num * q.num)) (q * q).den.sqrt = |q|
rw₂ : mkRat (Int.sqrt (q.num * q.num)) (q.den * q.den).sqrt = |q|
rw₃ : mkRat (↑q.num.natAbs : ℤ) (q.den * q.den).sqrt = |q|
rw₄ : mkRat (↑q.num.natAbs : ℤ) q.den = |q|
rw₅ : mkRat (↑q.num.natAbs : ℤ) q.den = (↑q.num.natAbs : ℤ) /. (↑q.den : ℤ)
rw₆ rw₇ : mkRat (↑q.num.natAbs : ℤ) q.den = mkRat (↑q.num.natAbs : ℤ) q.den
⊢ sqrt (q * q) = |q|

Tactic:
rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]

Premises used: Int.sqrt_eq, Rat.divInt_ofNat, Rat.abs_def, Rat.mul_self_num, Nat.sqrt_eq, Rat.sqrt, Rat.mul_self_den
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
x : ℚ
h : ∃ (q : ℚ), q * q = x
n : ℚ
hn : n * n = x
rw : sqrt (n * n) * sqrt (n * n) = n * n
rw₁ : |n| * |n| = n * n
rw₂ rw₃ : n * n = n * n
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, abs_mul_abs_self]

Premises used: abs_mul_abs_self, Rat.sqrt_eq
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
q : ℚ
⊢ 0 ≤ sqrt q

Tactic:
mkRat_nonneg (Int.sqrt_nonneg _) _

Premises used: Int.sqrt_nonneg, Rat.mkRat_nonneg, Rat.sqrt
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
m : ℚ
simp_rw : IsSquare m ↔ ∃ (q : ℚ), q * q = m
simp_rw₁ : (∃ (r : ℚ), m = r * r) ↔ ∃ (q : ℚ), q * q = m
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
simp_rw [← exists_mul_self m, IsSquare, eq_comm]

Premises used: eq_comm, IsSquare, Rat.exists_mul_self
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
z : ℤ
⊢ sqrt (↑z : ℚ) = (↑(Int.sqrt z) : ℚ)

Tactic:
simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]

Premises used: Rat.den_intCast, Rat.mkRat_one, Rat.sqrt, Nat.sqrt_one, Rat.num_intCast