awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = 0 ↔ x ≤ 0
⊢ √x = 0 ↔ x ≤ 0
have rw₁ : Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) (0 : ℝ≥0) ↔ x ≤ 0
Tactic: rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = 0 ↔ x ≤ 0
rw₁ : Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) (0 : ℝ≥0) ↔ x ≤ 0
⊢ √x = 0 ↔ x ≤ 0
have rw₂ : x.toNNReal = 0 ↔ x ≤ 0
Tactic: rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = 0 ↔ x ≤ 0
rw₁ : Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) (0 : ℝ≥0) ↔ x ≤ 0
rw₂ : x.toNNReal = 0 ↔ x ≤ 0
⊢ √x = 0 ↔ x ≤ 0
have rw₃ : x ≤ 0 ↔ x ≤ 0
Tactic: rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ √x ≠ 0 ↔ x ≠ 0
have rw : √x = 0 ↔ x = 0
Tactic: rw [not_iff_not, sqrt_eq_zero h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : √x = 0 ↔ x = 0
⊢ √x ≠ 0 ↔ x ≠ 0
have rw₁ : x = 0 ↔ x = 0
Tactic: rw [not_iff_not, sqrt_eq_zero h]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x ≠ 0 ↔ 0 < x
have rw : √x ≠ 0 ↔ ¬x ≤ 0
Tactic: rw [← not_le, not_iff_not, sqrt_eq_zero']
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √x ≠ 0 ↔ ¬x ≤ 0
⊢ √x ≠ 0 ↔ 0 < x
have rw₁ : √x = 0 ↔ x ≤ 0
Tactic: rw [← not_le, not_iff_not, sqrt_eq_zero']
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √x ≠ 0 ↔ ¬x ≤ 0
rw₁ : √x = 0 ↔ x ≤ 0
⊢ √x ≠ 0 ↔ 0 < x
have rw₂ : x ≤ 0 ↔ x ≤ 0
Tactic: rw [← not_le, not_iff_not, sqrt_eq_zero']
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0
have inl : x < 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
Tactic: rcases lt_trichotomy x 0 with _ | _ | _
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
inl : x < 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0
have inr : x = 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
Tactic: rcases lt_trichotomy x 0 with _ | _ | _
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
inl : x < 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
inr : x = 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0
have inr₁ : 0 < x → HPow.hPow (β := ℕ) (√x) 2 = max x 0
Tactic: rcases lt_trichotomy x 0 with _ | _ | _
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 < x
⊢ √x ≤ √y ↔ x ≤ y
have inl : ∀ (hy : y ≤ 0), √x ≤ √y ↔ x ≤ y
Tactic: obtain hy | hy := le_total y 0
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 < x
inl : ∀ (hy : y ≤ 0), √x ≤ √y ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y
have inr : ∀ (hy : 0 ≤ y), √x ≤ √y ↔ x ≤ y
Tactic: obtain hy | hy := le_total y 0
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ 1 ≤ √x ↔ 1 ≤ x
have rw : √1 ≤ √x ↔ √1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √1 ≤ √x ↔ √1 ≤ x
⊢ 1 ≤ √x ↔ 1 ≤ x
have rw₁ : 1 ≤ x ↔ √1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √1 ≤ √x ↔ √1 ≤ x
rw₁ : 1 ≤ x ↔ √1 ≤ x
⊢ 1 ≤ √x ↔ 1 ≤ x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x ≤ 1 ↔ x ≤ 1
have rw : √x ≤ √1 ↔ x ≤ √1
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √x ≤ √1 ↔ x ≤ √1
⊢ √x ≤ 1 ↔ x ≤ 1
have rw₁ : x ≤ 1 ↔ x ≤ √1
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : √x ≤ √1 ↔ x ≤ √1
rw₁ : x ≤ 1 ↔ x ≤ √1
⊢ √x ≤ 1 ↔ x ≤ 1
have rw₂ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ 1 < √2
have rw : √1 < √2
Tactic: rw [← Real.sqrt_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ √1 < √2
have h : LT.lt (α := ℝ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
⊢ √2 < 3 / 2
have rw : HPow.hPow (β := ℕ) (√2) 2 < HPow.hPow (β := ℕ) (3 / 2) 2
Tactic: rw [← sq_lt_sq₀ (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y
have simp_rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ)
Tactic: simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
simp_rw :
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ)
⊢ √(x * y) = √x * √y
have simp_rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
  (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)) :
    ℝ)
Tactic: simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
simp_rw :
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ)
simp_rw₁ :
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
    (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)) :
      ℝ)
⊢ √(x * y) = √x * √y
have simp_rw₂ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)
Tactic: simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
simp_rw :
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ)
simp_rw₁ :
  (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal) : ℝ) =
    (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)) :
      ℝ)
simp_rw₂ :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x * y).toNNReal =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)
⊢ √(x * y) = √x * √y
have simp_rw₃ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (x.toNNReal * y.toNNReal) =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0)
Tactic: simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ √(x * y) = √x * √y
have rw : √(y * x) = √x * √y
Tactic: rw [mul_comm, sqrt_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(y * x) = √x * √y
⊢ √(x * y) = √x * √y
have rw₁ : √y * √x = √x * √y
Tactic: rw [mul_comm, sqrt_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(y * x) = √x * √y
rw₁ : √y * √x = √x * √y
⊢ √(x * y) = √x * √y
have rw₂ : √x * √y = √x * √y
Tactic: rw [mul_comm, sqrt_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x⁻¹ = (√x)⁻¹
have rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹.toNNReal) : ℝ) = (√x)⁻¹
Tactic: rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹.toNNReal) : ℝ) = (√x)⁻¹
⊢ √x⁻¹ = (√x)⁻¹
have rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal⁻¹) : ℝ) = (√x)⁻¹
Tactic: rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹.toNNReal) : ℝ) = (√x)⁻¹
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal⁻¹) : ℝ) = (√x)⁻¹
⊢ √x⁻¹ = (√x)⁻¹
have rw₂ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal)⁻¹ : ℝ) = (√x)⁻¹
Tactic: rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹.toNNReal) : ℝ) = (√x)⁻¹
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal⁻¹) : ℝ) = (√x)⁻¹
rw₂ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal)⁻¹ : ℝ) = (√x)⁻¹
⊢ √x⁻¹ = (√x)⁻¹
have rw₃ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹ = (√x)⁻¹
Tactic: rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹.toNNReal) : ℝ) = (√x)⁻¹
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal⁻¹) : ℝ) = (√x)⁻¹
rw₂ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal)⁻¹ : ℝ) = (√x)⁻¹
rw₃ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹ = (√x)⁻¹
⊢ √x⁻¹ = (√x)⁻¹
have rw₄ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹ = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹
Tactic: rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x / y) = √x / √y
have rw : √(x * y⁻¹) = √x / √y
Tactic: rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : √(x * y⁻¹) = √x / √y
⊢ √(x / y) = √x / √y
have rw₁ : √x * √y⁻¹ = √x / √y
Tactic: rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
⊢ √(x / y) = √x / √y
have rw₂ : √x * (√y)⁻¹ = √x / √y
Tactic: rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
rw₂ : √x * (√y)⁻¹ = √x / √y
⊢ √(x / y) = √x / √y
have rw₃ : √x * (√y)⁻¹ = √x * (√y)⁻¹
Tactic: rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ √(x / y) = √x / √y
have rw : √(x * y⁻¹) = √x / √y
Tactic: rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(x * y⁻¹) = √x / √y
⊢ √(x / y) = √x / √y
have rw₁ : √x * √y⁻¹ = √x / √y
Tactic: rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
⊢ √(x / y) = √x / √y
have rw₂ : √x * (√y)⁻¹ = √x / √y
Tactic: rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
rw₂ : √x * (√y)⁻¹ = √x / √y
⊢ √(x / y) = √x / √y
have rw₃ : √x * (√y)⁻¹ = √x * (√y)⁻¹
Tactic: rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x / x = 1 / √x
have rw : x / √x / x = 1 / (x / √x)
Tactic: rw [← div_sqrt, one_div_div, div_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : x / √x / x = 1 / (x / √x)
⊢ √x / x = 1 / √x
have rw₁ : x / √x / x = √x / x
Tactic: rw [← div_sqrt, one_div_div, div_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : x / √x / x = 1 / (x / √x)
rw₁ : x / √x / x = √x / x
⊢ √x / x = 1 / √x
have rw₂ : √x / x = √x / x
Tactic: rw [← div_sqrt, one_div_div, div_sqrt]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
⊢ √x / x = (√x)⁻¹
have rw : 1 / √x = (√x)⁻¹
Tactic: rw [sqrt_div_self', one_div]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
rw : 1 / √x = (√x)⁻¹
⊢ √x / x = (√x)⁻¹
have rw₁ : (√x)⁻¹ = (√x)⁻¹
Tactic: rw [sqrt_div_self', one_div]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ x < √y ↔ HPow.hPow (β := ℕ) x 2 < y
have rw : x < √y ↔ √(HPow.hPow (β := ℕ) x 2) < √y
Tactic: rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
rw : x < √y ↔ √(HPow.hPow (β := ℕ) x 2) < √y
⊢ x < √y ↔ HPow.hPow (β := ℕ) x 2 < y
have rw₁ : x < √y ↔ x < √y
Tactic: rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
⊢ HPow.hPow (β := ℕ) x 2 < y ↔ -√y < x ∧ x < √y
have rw : HPow.hPow (β := ℕ) x 2 < y ↔ |x| < √y
Tactic: rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
rw : HPow.hPow (β := ℕ) x 2 < y ↔ |x| < √y
⊢ HPow.hPow (β := ℕ) x 2 < y ↔ -√y < x ∧ x < √y
have rw₁ : HPow.hPow (β := ℕ) |x| 2 < y ↔ |x| < √y
Tactic: rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
rw : HPow.hPow (β := ℕ) x 2 < y ↔ |x| < √y
rw₁ : HPow.hPow (β := ℕ) |x| 2 < y ↔ |x| < √y
⊢ HPow.hPow (β := ℕ) x 2 < y ↔ -√y < x ∧ x < √y
have rw₂ : HPow.hPow (β := ℕ) |x| 2 < y ↔ HPow.hPow (β := ℕ) |x| 2 < y
Tactic: rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (hypothesis)
Goal:
x y : ℝ
h : √x < y
⊢ x < HPow.hPow (β := ℕ) y 2
have hy : 0 < y
Tactic: have hy := x.sqrt_nonneg.trans_lt h
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < HPow.hPow (β := ℕ) y 2
have rwa : √x < √(HPow.hPow (β := ℕ) y 2)
Tactic: rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ (↑a.sqrt : ℝ) ≤ √(↑a : ℝ)
have rw : HPow.hPow (α := ℝ) (β := ℕ) (↑a.sqrt : ℝ) 2 ≤ (↑a : ℝ)
Tactic: rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑a.sqrt : ℝ) 2 ≤ (↑a : ℝ)
have norm_cast : HPow.hPow (β := ℕ) a.sqrt 2 ≤ a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
have rw : (↑a : ℝ) < HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1) 2
Tactic: rw [sqrt_lt (by simp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
rw : (↑a : ℝ) < HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1) 2
⊢ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
have rw₁ : 0 ≤ HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
Tactic: rw [sqrt_lt (by simp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ (↑a : ℝ) < HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1) 2
have norm_cast : a < HPow.hPow (β := ℕ) (a.sqrt + 1) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
have norm_cast : 0 ≤ a.sqrt + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ ⌊√(↑a : ℝ)⌋ = (↑a.sqrt : ℤ)
have rw : (↑(↑a.sqrt : ℤ) : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑(↑a.sqrt : ℤ) : ℝ) 1
Tactic: rw [Int.floor_eq_iff]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
a : ℕ
⊢ ⌊√(↑a : ℝ)⌋₊ = a.sqrt
have rw : (↑a.sqrt : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
Tactic: rw [Nat.floor_eq_iff (sqrt_nonneg a)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
⊢ 0 ≤ 1 + x / 2
have linarith : 1 + x / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
linarith : 1 + x / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ 1 + x / 2
have linarith₁ : 1 + x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
linarith : 1 + x / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 + x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ 1 + x / 2
have linarith₂ : 1 + x / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
linarith : 1 + x / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 + x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 + x / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 + x / 2
have linarith₃ : 1 + x / 2 < 0 → -1 + (-1 - x) + (HMul.hMul (α := ℝ) 2 1 + 1 * x - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
⊢ √(1 + x) ≤ 1 + x / 2
have refine : 1 + x ≤ HPow.hPow (β := ℕ) (1 + x / 2) 2
Tactic: refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ
h : -1 ≤ x
⊢ 1 + x ≤ HPow.hPow (β := ℕ) (1 + x / 2) 2
have calc : 1 + x + HPow.hPow (β := ℕ) (x / 2) 2 = HPow.hPow (β := ℕ) (1 + x / 2) 2
Tactic: calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = ∏ i ∈ s, √(x i)
have h : √(∏ i ∈ s, x i) = (↑((NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) (∏ x_1 ∈ s, (toNNReal ∘ x) x_1)) : ℝ)
Tactic: convert! congr_arg NNReal.toReal <| map_prod NNReal.sqrtHom (Real.toNNReal ∘ x) s
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
h : √(∏ i ∈ s, x i) = (↑((NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) (∏ x_1 ∈ s, (toNNReal ∘ x) x_1)) : ℝ)
⊢ √(∏ i ∈ s, x i) = ∏ i ∈ s, √(x i)
have h₁ : ∏ i ∈ s, √(x i) = (↑(∏ x_1 ∈ s, (NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) ((toNNReal ∘ x) x_1)) : ℝ)
Tactic: convert! congr_arg NNReal.toReal <| map_prod NNReal.sqrtHom (Real.toNNReal ∘ x) s
-- Lean 4 proof step from Mathlib.Data.Real.StarOrdered (goal)
Goal:
r : ℝ
⊢ 0 ≤ r ↔ ∃ (s : ℝ), r = star s * s
have refine : (∃ (s : ℝ), r = star s * s) → 0 ≤ r
Tactic: refine ⟨fun hr => ⟨√r, (mul_self_sqrt hr).symm⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.StarOrdered (goal)
Goal:
⊢ StarOrderedRing ℝ≥0
have refine_1 : ∀ (x y : ℝ≥0) (h : x ≤ y), ∃ (s : ℝ≥0), y = x + star s * s
Tactic: refine .of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.StarOrdered (goal)
Goal:
refine_1 : ∀ (x y : ℝ≥0) (h : x ≤ y), ∃ (s : ℝ≥0), y = x + star s * s
⊢ StarOrderedRing ℝ≥0
have refine_2 : ∀ (x y : ℝ≥0), (∃ (s : ℝ≥0), y = x + star s * s) → x ≤ y
Tactic: refine .of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.StarOrdered (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ ∃ (s : ℝ≥0), y = x + star s * s
have refine_1 : ∀ (d : ℝ≥0) (h : x ≤ x + d), ∃ (s : ℝ≥0), x + d = x + star s * s
Tactic: obtain ⟨d, rfl⟩ := exists_add_of_le h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Real.StarOrdered (goal)
Goal:
x d : ℝ≥0
h : x ≤ x + d
⊢ ∃ (s : ℝ≥0), x + d = x + star s * s
have refine_1 : x + d = x + HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (star ((sqrt : (a : ℝ≥0) → ℝ≥0) d) : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) d : ℝ≥0)
Tactic: refine ⟨sqrt d, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Rel.Cover (goal)
Goal:
X : Type u_1
U : SetRel X X
s N : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
hN : Maximal (fun (N : Set X) ↦ N ⊆ s ∧ U.IsSeparated N) N
x : X
hx : x ∈ s
⊢ ∃ (y : X), y ∈ N ∧ (x, y) ∈ U
have by_contra! : ∀ (h : ∀ (y : X) (_ : y ∈ N), ¬(x, y) ∈ U), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u
have pos : ∀ (hst : Disjoint t₁ t₂), s ×ˢ t₁ ○ t₂ ×ˢ u = ∅
Tactic: split_ifs with hst
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
pos : ∀ (hst : Disjoint t₁ t₂), s ×ˢ t₁ ○ t₂ ×ˢ u = ∅
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u
have neg : ∀ (hst : ¬Disjoint t₁ t₂), s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
Tactic: split_ifs with hst
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
have neg : s ×ˢ u = s ×ˢ u
Tactic: rw [prod_comp_prod_of_inter_nonempty <| Set.not_disjoint_iff_nonempty_inter.1 hst]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
⊢ ∃ (x : α), s = {x} ∧ t = {x}
have obtain : ∀ (a : α) (ha : a ∈ s), ∃ (x : α), s = {x} ∧ t = {x}
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
a : α
ha : a ∈ s
⊢ ∃ (x : α), s = {x} ∧ t = {x}
have obtain : ∀ (b : α) (hb : b ∈ t), ∃ (x : α), s = {x} ∧ t = {x}
Tactic: obtain ⟨b, hb⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Rel (hypothesis)
Goal:
α : Type u_1
s t : Set α
hst : s ×ˢ t ⊆ SetRel.id
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ (x : α), s = {x} ∧ t = {x}
have hst₁ : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
Tactic: simp only [Set.prod_subset_iff, mem_id] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Rel (hypothesis)
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
⊢ ∃ (x : α), s = {x} ∧ t = {x}
have hb₁ : a ∈ t
Tactic: obtain rfl := hst _ ha _ hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
hb : a ∈ t
⊢ ∃ (x : α), s = {x} ∧ t = {x}
have simp : ∃ (x : α), x ∈ s ∧ (∀ (x_1 : α), x_1 ∈ s → x_1 = x) ∧ x ∈ t ∧ ∀ (x_1 : α), x_1 ∈ t → x_1 = x
Tactic: simp only [Set.eq_singleton_iff_unique_mem, and_assoc]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsSymm
⊢ R.inv = R
have h : ∀ (x : α × α), x ∈ R.inv ↔ x ∈ R
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
R : SetRel α α
hR : R.inv = R
a b : α
hab : (a, b) ∈ R
⊢ (b, a) ∈ R
have rwa : (b, a) ∈ R.inv
Tactic: rwa [← hR]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst : R.IsSymm
⊢ ∀ (a b : β), (a, b) ∈ Prod.map f f '' R → (b, a) ∈ Prod.map f f '' R
have simp : ∀ (a b : β) (x x_1 : α),
  (x, x_1) ∈ R → f x = a → f x_1 = b → ∃ (a_5 : α), ∃ (b_2 : α), (a_5, b_2) ∈ R ∧ f a_5 = b ∧ f b_2 = a
Tactic: simp only [Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq, forall_exists_index,
      and_imp]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]