awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ b = d
have right : (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).den : ℤ) = d
Tactic: rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ b = d
have right₁ : (↑(HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)).den : ℤ) = d
Tactic: rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ b = d
have right₂ : d = d
Tactic: rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
have pos : ∀ (hn : n = 0), (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
pos : ∀ (hn : n = 0), (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
have neg : ∀ (hn : ¬n = 0), (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
hn : n = 0
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
have pos : (↑(0 / 0) : ℚ) = HDiv.hDiv (α := ℚ) (↑0 : ℚ) (↑0 : ℚ)
Tactic: subst hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
hn : ¬n = 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0
have rwa : ∀ (hn : ¬Eq (α := ℚ) (↑n : ℚ) (↑0 : ℚ)), Ne (α := ℚ) (↑n : ℚ) 0
Tactic: rwa [← coe_int_inj] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
n : ℤ
hn : ¬n = 0
⊢ (↑(n / n) : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n : ℚ)
have this : Ne (α := ℚ) (↑n : ℚ) 0
Tactic: have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
h : b ∣ a
⊢ (↑(a / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)
have rcases : ∀ (c : ℤ), (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
Tactic: rcases h with ⟨c, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
b c : ℤ
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw : (↑(c * b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
b c : ℤ
rw : (↑(c * b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw₁ : (↑(c * (b / b)) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
b c : ℤ
rw : (↑(c * b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
rw₁ : (↑(c * (b / b)) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑b : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw₂ : HMul.hMul (α := ℚ) (↑c : ℚ) (↑(b / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw₃ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(c * b) : ℚ) (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw₄ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = HMul.hMul (α := ℚ) (↑c : ℚ) (↑b : ℚ) / (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ (↑(b * c / b) : ℚ) = HDiv.hDiv (α := ℚ) (↑(b * c) : ℚ) (↑b : ℚ)
have rw₅ : (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑b : ℚ) = (↑c : ℚ) * HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑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]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
m n : ℤ
hn : n ≠ 0
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 ↔ n ∣ m
have hn₁ : Ne (α := ℚ) (↑n : ℚ) 0
Tactic: replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 ↔ n ∣ m
have mp : (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 → n ∣ m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
mp : (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 → n ∣ m
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 ↔ n ∣ m
have mpr : n ∣ m → (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
m n : ℤ
hn : Ne (α := ℚ) (↑n : ℚ) 0
⊢ (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).den = 1 → n ∣ m
have mp : HMul.hMul (α := ℚ) (↑(HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑n : ℚ)).num : ℚ) (↑n : ℚ) = (↑m : ℚ) → n ∣ m
Tactic: rw [Rat.den_eq_one_iff, eq_div_iff hn]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℤ
ha0 : 0 < a
⊢ (↑(den (↑a : ℚ)⁻¹) : ℤ) = a
have simp : (↑(if a = 0 then 1 else a.natAbs) : ℤ) = a
Tactic: simp only [den_inv, num_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℕ
ha0 : 0 < a
⊢ den (↑a : ℚ)⁻¹ = a
have rw : LT.lt (α := ℤ) 0 (↑a : ℤ)
Tactic: rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ num (OfNat.ofNat a)⁻¹ = 1
have this : 2 ≤ a
Tactic: have : 2 ≤ a := Nat.AtLeastTwo.prop
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℕ
inst : a.AtLeastTwo
this : 2 ≤ a
⊢ num (OfNat.ofNat a)⁻¹ = 1
have simp : LT.lt (α := ℤ) 0 (OfNat.ofNat a)
Tactic: simp only [num_inv, num_ofNat, den_ofNat, Nat.cast_one, mul_one, Int.sign_eq_one_iff_pos,
    gt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ)) 2 ≤ (↑x : ℚ)
have rw : HPow.hPow (α := ℚ) (β := ℕ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 2 ≤
  (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2
Tactic: rw [div_pow, div_le_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 2 ≤
    (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2
have norm_cast : HPow.hPow (β := ℕ) (x * HPow.hPow (β := ℕ) prec 2).sqrt 2 ≤ x * HPow.hPow (β := ℕ) prec 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑x : ℚ) <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
have 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
Tactic: rw [← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑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
have rw : (↑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 [← mul_pow, add_mul]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) * (↑prec : ℚ) +
        HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ) * (↑prec : ℚ))
      2
have rw : (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 1) 2
Tactic: rw [div_mul_cancel₀, div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
rw :
  (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 1) 2
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) (↑prec : ℚ) * (↑prec : ℚ) +
        HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ) * (↑prec : ℚ))
      2
have h₁ : Ne (α := ℚ) (↑prec : ℚ) 0
Tactic: rw [div_mul_cancel₀, div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑x : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑prec : ℚ) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑(x * HPow.hPow (β := ℕ) prec 2).sqrt : ℚ) 1) 2
have norm_cast : x * HPow.hPow (β := ℕ) prec 2 < HPow.hPow (β := ℕ) ((x * HPow.hPow (β := ℕ) prec 2).sqrt + 1) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Defs (goal)
Goal:
x prec : ℕ
h : 0 < prec
⊢ Ne (α := ℚ) (↑prec : ℚ) 0
have h₁ : ¬prec = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
Goal:
x prec : ℕ
h : 0 < prec
⊢ (↑(x.ratSqrt prec) : ℝ) ≤ √(↑x : ℝ)
have this : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
Tactic: have := ratSqrt_sq_le (x := x) h
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
Goal:
x prec : ℕ
h : 0 < prec
this : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
⊢ (↑(x.ratSqrt prec) : ℝ) ≤ √(↑x : ℝ)
have this₁ : HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)
Tactic: have : (x.ratSqrt prec ^ 2 : ℝ) ≤ ↑x := by norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
Goal:
x prec : ℕ
h : 0 < prec
this_1 : HPow.hPow (β := ℕ) (x.ratSqrt prec) 2 ≤ (↑x : ℚ)
this : HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2 ≤ (↑x : ℝ)
⊢ (↑(x.ratSqrt prec) : ℝ) ≤ √(↑x : ℝ)
have this₁ : √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec) : ℝ) 2) ≤ √(↑x : ℝ)
Tactic: have := Real.sqrt_monotone this
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (goal)
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 : ℝ)
⊢ (↑(x.ratSqrt prec) : ℝ) ≤ √(↑x : ℝ)
have rwa : LE.le (α := ℝ) 0 (↑(x.ratSqrt prec) : ℝ)
Tactic: rwa [Real.sqrt_sq] at this
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
Goal:
x prec : ℕ
h : 0 < prec
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
have this : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
Tactic: have := lt_ratSqrt_add_inv_prec_sq (x := x) h
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
Goal:
x prec : ℕ
h : 0 < prec
this : (↑x : ℚ) < HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (hypothesis)
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 : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
have this₁ : √(↑x : ℝ) < √(↑(HPow.hPow (β := ℕ) (x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) 2) : ℝ)
Tactic: have := Real.sqrt_lt_sqrt (by simp) this
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (goal)
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) : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
have rw : ∀ (this : √(↑x : ℝ) < (↑(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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (goal)
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 : ℝ)
⊢ √(↑x : ℝ) < (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
have rw₁ : ∀ (this : √(↑x : ℝ) < √(HPow.hPow (α := ℝ) (β := ℕ) (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ) 2)),
  LE.le (α := ℝ) 0 (↑(x.ratSqrt prec + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)
Tactic: rw [Rat.cast_pow, Real.sqrt_sq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.NatSqrt.Real (goal)
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 + HDiv.hDiv (α := ℚ) 1 (↑prec : ℚ)) : ℝ)
have push_cast : 0 ≤ (↑(x.ratSqrt prec) : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑prec : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
q : ℚ
⊢ sqrt (q * q) = |q|
have rw : mkRat (Int.sqrt (q * q).num) (q * q).den.sqrt = |q|
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
q : ℚ
rw : mkRat (Int.sqrt (q * q).num) (q * q).den.sqrt = |q|
⊢ sqrt (q * q) = |q|
have rw₁ : mkRat (Int.sqrt (q.num * q.num)) (q * q).den.sqrt = |q|
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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|
⊢ sqrt (q * q) = |q|
have rw₂ : mkRat (Int.sqrt (q.num * q.num)) (q.den * q.den).sqrt = |q|
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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|
⊢ sqrt (q * q) = |q|
have rw₃ : mkRat (↑q.num.natAbs : ℤ) (q.den * q.den).sqrt = |q|
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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|
⊢ sqrt (q * q) = |q|
have rw₄ : mkRat (↑q.num.natAbs : ℤ) q.den = |q|
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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|
⊢ sqrt (q * q) = |q|
have rw₅ : mkRat (↑q.num.natAbs : ℤ) q.den = (↑q.num.natAbs : ℤ) /. (↑q.den : ℤ)
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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 : ℤ)
⊢ sqrt (q * q) = |q|
have rw₆ : mkRat (↑q.num.natAbs : ℤ) q.den = mkRat (↑q.num.natAbs : ℤ) q.den
Tactic: rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
x : ℚ
h : ∃ (q : ℚ), q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x
have rw : sqrt (n * n) * sqrt (n * n) = n * n
Tactic: rw [← hn, sqrt_eq, abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
x : ℚ
h : ∃ (q : ℚ), q * q = x
n : ℚ
hn : n * n = x
rw : sqrt (n * n) * sqrt (n * n) = n * n
⊢ sqrt x * sqrt x = x
have rw₁ : |n| * |n| = n * n
Tactic: rw [← hn, sqrt_eq, abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
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
⊢ sqrt x * sqrt x = x
have rw₂ : n * n = n * n
Tactic: rw [← hn, sqrt_eq, abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
m : ℚ
⊢ IsSquare m ↔ sqrt m * sqrt m = m
have simp_rw : IsSquare m ↔ ∃ (q : ℚ), q * q = m
Tactic: simp_rw [← exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
m : ℚ
simp_rw : IsSquare m ↔ ∃ (q : ℚ), q * q = m
⊢ IsSquare m ↔ sqrt m * sqrt m = m
have simp_rw₁ : (∃ (r : ℚ), m = r * r) ↔ ∃ (q : ℚ), q * q = m
Tactic: simp_rw [← exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
n : ℕ
⊢ sqrt (↑n : ℚ) = (↑n.sqrt : ℚ)
have rw : sqrt (↑(↑n : ℤ) : ℚ) = (↑n.sqrt : ℚ)
Tactic: rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
n : ℕ
rw : sqrt (↑(↑n : ℤ) : ℚ) = (↑n.sqrt : ℚ)
⊢ sqrt (↑n : ℚ) = (↑n.sqrt : ℚ)
have rw₁ : Eq (α := ℚ) (↑(Int.sqrt (↑n : ℤ)) : ℚ) (↑n.sqrt : ℚ)
Tactic: rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
n : ℕ
rw : sqrt (↑(↑n : ℤ) : ℚ) = (↑n.sqrt : ℚ)
rw₁ : Eq (α := ℚ) (↑(Int.sqrt (↑n : ℤ)) : ℚ) (↑n.sqrt : ℚ)
⊢ sqrt (↑n : ℚ) = (↑n.sqrt : ℚ)
have rw₂ : Eq (α := ℚ) (↑(↑n.sqrt : ℤ) : ℚ) (↑n.sqrt : ℚ)
Tactic: rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Sqrt (goal)
Goal:
n : ℕ
rw : sqrt (↑(↑n : ℤ) : ℚ) = (↑n.sqrt : ℚ)
rw₁ : Eq (α := ℚ) (↑(Int.sqrt (↑n : ℤ)) : ℚ) (↑n.sqrt : ℚ)
rw₂ : Eq (α := ℚ) (↑(↑n.sqrt : ℤ) : ℚ) (↑n.sqrt : ℚ)
⊢ sqrt (↑n : ℚ) = (↑n.sqrt : ℚ)
have rw₃ : Eq (α := ℚ) (↑n.sqrt : ℚ) (↑n.sqrt : ℚ)
Tactic: rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
⊢ Eq (α := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) ⊤
have refine : ∀ (x : ℚ≥0), Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x
Tactic: refine (eq_top_iff' _).2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x
have rw : Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n))
  ((x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x
have suffices : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
Tactic: suffices x = (x.num * x.den ^ (n - 1)) • (x.den : ℚ≥0)⁻¹ ^ n by
    rw [this]
    exact nsmul_mem (subset_closure <| mem_range_self _) _
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = (↑(x.num * x.den ^ (n - 1)) : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
have push_cast : x = (↑x.num : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0) (n - 1) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = (↑x.num : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0) (n - 1) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
have rw : Ne (α := ℚ≥0) (↑x.den : ℚ≥0) 0
Tactic: rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul,
    ← div_eq_mul_inv, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
rw ha : Ne (α := ℚ≥0) (↑x.den : ℚ≥0) 0
⊢ x = (↑x.num : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0) (n - 1) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
have h : 1 ≤ n
Tactic: rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul,
    ← div_eq_mul_inv, num_div_den]