awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw : HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 = x
⊢ HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) = x
have rw₁ : x = x
Tactic: rw [← sq, sq_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * x) = x
have rw : (sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) x 2) = x
Tactic: rw [← sq, sqrt_sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw : (sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) x 2) = x
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * x) = x
have rw₁ : x = x
Tactic: rw [← sq, sqrt_sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
⊢ LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ↔ x ≤ 1
have rw : LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ↔ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ↔
    x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
⊢ LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ↔ x ≤ 1
have rw₁ : x ≤ 1 ↔ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ↔
    x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
rw₁ : x ≤ 1 ↔ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
⊢ LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ↔ x ≤ 1
have rw₂ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ 1 ≤ x
have rw : LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔
    (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ 1 ≤ x
have rw₁ : 1 ≤ x ↔ (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔
    (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
rw₁ : 1 ≤ x ↔ (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ 1 ≤ x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ≤ max x y
have rw : x * y ≤ max x y * max x y
Tactic: rw [sqrt_le_iff_le_sq, sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
⊢ x * y ≤ max x y * max x y
have h₁ : x ≤ max x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
h₁ : x ≤ max x y
⊢ x * y ≤ max x y * max x y
have h₂ : y ≤ max x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
have rw : x * y =
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)) 2
Tactic: rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
rw :
  x * y =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)) 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
have rw₁ : x * y =
  HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 *
    HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
Tactic: rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
rw :
  x * y =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)) 2
rw₁ :
  x * y =
    HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 *
      HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
have rw₂ : x * y = x * HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
Tactic: rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ≥0
rw :
  x * y =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)) 2
rw₁ :
  x * y =
    HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 *
      HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
rw₂ : x * y = x * HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
have rw₃ : x * y = x * y
Tactic: rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
⊢ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = √(↑x : ℝ)
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑x : ℝ).toNNReal) : ℝ)
Tactic: rw [Real.sqrt, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑x : ℝ).toNNReal) : ℝ)
⊢ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = √(↑x : ℝ)
have rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ)
Tactic: rw [Real.sqrt, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ √x
have unfold : Continuous (Y := ℝ) fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)
Tactic: unfold sqrt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ Eq (α := Filter ℝ) (map (fun (x : ℝ) ↦ √x) atTop) atTop
have unfold : Eq (α := Filter ℝ) (map (fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)) atTop) atTop
Tactic: unfold sqrt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ Eq (α := Filter ℝ) (comap (β := ℝ) (fun (x : ℝ) ↦ √x) atTop) atTop
have unfold : Eq (α := Filter ℝ) (comap (β := ℝ) (fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)) atTop) atTop
Tactic: unfold sqrt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ 0 ≤ √x
have unfold : 0 ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)
Tactic: unfold sqrt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ √x * √x = x
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = x
Tactic: rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = x
⊢ √x * √x = x
have rw₁ : (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)) :
    ℝ) =
  x
Tactic: rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = x
rw₁ :
  (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)) :
      ℝ) =
    x
⊢ √x * √x = x
have rw₂ : (↑x.toNNReal : ℝ) = x
Tactic: rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = x
rw₁ :
  (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)) :
      ℝ) =
    x
rw₂ : (↑x.toNNReal : ℝ) = x
⊢ √x * √x = x
have rw₃ : x = x
Tactic: rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
⊢ √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
have mp : √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
mp : √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
⊢ √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
have mpr : y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
have mp : ∀ (hle : 0 ≤ x), √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Tactic: rcases le_or_gt 0 x with hle | hlt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
mp : ∀ (hle : 0 ≤ x), √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
have mp₁ : ∀ (hlt : x < 0), √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Tactic: rcases le_or_gt 0 x with hle | hlt
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
⊢ x = y * y
have rw : x = √x * √x
Tactic: rw [← h, mul_self_sqrt hx]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
rw : x = √x * √x
⊢ x = y * y
have rw₁ : x = x
Tactic: rw [← h, mul_self_sqrt hx]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ √x = y
have rw : √(y * y) = y
Tactic: rw [h, sqrt_mul_self hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
rw : √(y * y) = y
⊢ √x = y
have rw₁ : y = y
Tactic: rw [h, sqrt_mul_self hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ HMul.hMul (α := ℝ) 1 1 = x ↔ x = 1
have rw : x = HMul.hMul (α := ℝ) 1 1 ↔ x = 1
Tactic: rw [eq_comm, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : x = HMul.hMul (α := ℝ) 1 1 ↔ x = 1
⊢ HMul.hMul (α := ℝ) 1 1 = x ↔ x = 1
have rw₁ : x = 1 ↔ x = 1
Tactic: rw [eq_comm, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ HPow.hPow (β := ℕ) (√x) 2 = x
have rw : √x * √x = x
Tactic: rw [sq, mul_self_sqrt h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : √x * √x = x
⊢ HPow.hPow (β := ℕ) (√x) 2 = x
have rw₁ : x = x
Tactic: rw [sq, mul_self_sqrt h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ √(HPow.hPow (β := ℕ) x 2) = x
have rw : √(x * x) = x
Tactic: rw [sq, sqrt_mul_self h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : √(x * x) = x
⊢ √(HPow.hPow (β := ℕ) x 2) = x
have rw₁ : x = x
Tactic: rw [sq, sqrt_mul_self h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ x = HPow.hPow (β := ℕ) y 2
have rw : √x = y ↔ x = y * y
Tactic: rw [sq, sqrt_eq_iff_mul_self_eq hx hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
rw : √x = y ↔ x = y * y
⊢ √x = y ↔ x = HPow.hPow (β := ℕ) y 2
have rw₁ : x = y * y ↔ x = y * y
Tactic: rw [sq, sqrt_eq_iff_mul_self_eq hx hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √(x * x) = |x|
have rw : √(|x| * |x|) = |x|
Tactic: rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √(|x| * |x|) = |x|
⊢ √(x * x) = |x|
have rw₁ : |x| = |x|
Tactic: rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √(HPow.hPow (β := ℕ) x 2) = |x|
have rw : √(x * x) = |x|
Tactic: rw [sq, sqrt_mul_self_eq_abs]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √(x * x) = |x|
⊢ √(HPow.hPow (β := ℕ) x 2) = |x|
have rw₁ : |x| = |x|
Tactic: rw [sq, sqrt_mul_self_eq_abs]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x ≤ y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have rw₂ : LE.le (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
  x ≤ y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x ≤ y
rw₂ :
  LE.le (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have rw₃ : x.toNNReal ≤ y.toNNReal ↔ x ≤ y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x ≤ y
rw₂ :
  LE.le (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x ≤ y
rw₃ : x.toNNReal ≤ y.toNNReal ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have rw₄ : x ≤ y ↔ x ≤ y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
⊢ √x < √y ↔ x < y
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
⊢ √x < √y ↔ x < y
have rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x < y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x < y
⊢ √x < √y ↔ x < y
have rw₂ : LT.lt (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
  x < y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x < y
rw₂ :
  LT.lt (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x < y
⊢ √x < √y ↔ x < y
have rw₃ : x.toNNReal < y.toNNReal ↔ x < y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x < y
rw₂ :
  LT.lt (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x < y
rw₃ : x.toNNReal < y.toNNReal ↔ x < y
⊢ √x < √y ↔ x < y
have rw₄ : x < y ↔ x < y
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : x ≤ y
⊢ √x ≤ √y
have rw : x.toNNReal ≤ y.toNNReal
Tactic: rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₃ : x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₃ : x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₄ : x.toNNReal ≤ (y * y).toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₃ : x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₄ : x.toNNReal ≤ (y * y).toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₅ : x ≤ y * y ↔ x ≤ HPow.hPow (β := ℕ) y 2
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₃ : x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₄ : x.toNNReal ≤ (y * y).toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₅ : x ≤ y * y ↔ x ≤ HPow.hPow (β := ℕ) y 2
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
have rw₆ : x ≤ y * y ↔ x ≤ y * y
Tactic: rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ HPow.hPow (β := ℕ) y 2
have rw : 0 ≤ y → (√x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2)
Tactic: rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2
have rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
Tactic: rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2
have rw₁ : √x < y ↔ √x < y
Tactic: rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2
have rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
Tactic: rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2
have rw₁ : √x < y ↔ √x < y
Tactic: rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
⊢ |x| ≤ √y
have rw : √(HPow.hPow (β := ℕ) x 2) ≤ √y
Tactic: rw [← sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : 0 ≤ y
⊢ HPow.hPow (β := ℕ) x 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y
have mp : HPow.hPow (β := ℕ) x 2 ≤ y → -√y ≤ x ∧ x ≤ √y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : 0 ≤ y
mp : HPow.hPow (β := ℕ) x 2 ≤ y → -√y ≤ x ∧ x ≤ √y
⊢ HPow.hPow (β := ℕ) x 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y
have mpr : -√y ≤ x ∧ x ≤ √y → HPow.hPow (β := ℕ) x 2 ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → HPow.hPow (β := ℕ) x 2 ≤ y
have mpr : |x| ≤ √y → HPow.hPow (β := ℕ) |x| 2 ≤ y
Tactic: rw [← abs_le, ← sq_abs]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x = 0 ↔ x ≤ 0
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = 0 ↔ x ≤ 0
Tactic: rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]