awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Sqrt
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)
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)
⊢ √(x * y) = √x * √y

Tactic:
simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]

Premises used: Real.toNNReal_mul, NNReal.sqrt_mul, Real.sqrt, NNReal.coe_mul, NNReal.coe_inj
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(y * x) = √x * √y
rw₁ : √y * √x = √x * √y
rw₂ rw₃ : √x * √y = √x * √y
⊢ √(x * y) = √x * √y

Tactic:
rw [mul_comm, sqrt_mul hy, mul_comm]

Premises used: Real.sqrt_mul, mul_comm
-- Module: Mathlib.Data.Real.Sqrt
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)⁻¹
rw₄ rw₅ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹ = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)⁻¹
⊢ √x⁻¹ = (√x)⁻¹

Tactic:
rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]

Premises used: Real.toNNReal_inv, NNReal.coe_inv, Real.sqrt, NNReal.sqrt_inv
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
rw₂ : √x * (√y)⁻¹ = √x / √y
rw₃ rw₄ : √x * (√y)⁻¹ = √x * (√y)⁻¹
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul hx, sqrt_inv, division_def]

Premises used: Real.sqrt_inv, Real.sqrt_mul, division_def
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 ≤ y
rw : √(x * y⁻¹) = √x / √y
rw₁ : √x * √y⁻¹ = √x / √y
rw₂ : √x * (√y)⁻¹ = √x / √y
rw₃ rw₄ : √x * (√y)⁻¹ = √x * (√y)⁻¹
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]

Premises used: Iff.mpr, Real.sqrt_inv, division_def, inv_nonneg, Real.sqrt_mul'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
⊢ x / √x = √x

Tactic:
grind
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : x / √x / x = 1 / (x / √x)
rw₁ : x / √x / x = √x / x
rw₂ rw₃ : √x / x = √x / x
⊢ √x / x = 1 / √x

Tactic:
rw [← div_sqrt, one_div_div, div_sqrt]

Premises used: Real.div_sqrt, one_div_div
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : 1 / √x = (√x)⁻¹
rw₁ rw₂ : (√x)⁻¹ = (√x)⁻¹
⊢ √x / x = (√x)⁻¹

Tactic:
rw [sqrt_div_self', one_div]

Premises used: Real.sqrt_div_self', one_div
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
rw : x < √y ↔ √(HPow.hPow (β := ℕ) x 2) < √y
rw₁ rw₂ : x < √y ↔ x < √y
⊢ x < √y ↔ HPow.hPow (β := ℕ) x 2 < y

Tactic:
rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]

Premises used: Real.sqrt_lt_sqrt_iff, sq_nonneg, Real.sqrt_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
rw : HPow.hPow (β := ℕ) x 2 < y ↔ |x| < √y
rw₁ : HPow.hPow (β := ℕ) |x| 2 < y ↔ |x| < √y
rw₂ rw₃ : HPow.hPow (β := ℕ) |x| 2 < y ↔ HPow.hPow (β := ℕ) |x| 2 < y
⊢ HPow.hPow (β := ℕ) x 2 < y ↔ -√y < x ∧ x < √y

Tactic:
rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]

Premises used: Real.lt_sqrt, abs_lt, sq_abs, abs_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 < y
⊢ -√y < x

Tactic:
(sq_lt.mp h).1

Premises used: Real.sq_lt, And.left, Iff.mp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 < y
⊢ x < √y

Tactic:
(sq_lt.mp h).2

Premises used: Real.sq_lt, And.right, Iff.mp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : √x < y
⊢ 0 < y

Tactic:
have hy := x.sqrt_nonneg.trans_lt h
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : √x < y
hy : 0 < y
rwa : √x < √(HPow.hPow (β := ℕ) y 2)
rwa₁ rwa₂ rwa₃ rwa₄ : √x < y
⊢ x < HPow.hPow (β := ℕ) y 2

Tactic:
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]

Premises used: Real.sqrt_lt_sqrt_iff_of_pos, sq_pos_of_pos, LT.lt.le, Real.sqrt_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
rw : HPow.hPow (α := ℝ) (β := ℕ) (↑a.sqrt : ℝ) 2 ≤ (↑a : ℝ)
⊢ (↑a.sqrt : ℝ) ≤ √(↑a : ℝ)

Tactic:
rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]

Premises used: Nat.cast_nonneg, Real.le_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
norm_cast : HPow.hPow (β := ℕ) a.sqrt 2 ≤ a
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑a.sqrt : ℝ) 2 ≤ (↑a : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ HPow.hPow (β := ℕ) a.sqrt 2 ≤ a

Tactic:
Nat.sqrt_le' a

Premises used: Nat.sqrt_le'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ HPow.hPow (β := ℕ) a.sqrt 2 ≤ a

Tactic:
exact Nat.sqrt_le' a

Premises used: Nat.sqrt_le'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ LE.le (α := ℝ) 0 (↑a : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
rw : (↑a : ℝ) < HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1) 2
rw₁ : 0 ≤ HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
⊢ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1

Tactic:
rw [sqrt_lt (by simp)]

Premises used: Real.sqrt_lt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
norm_cast : a < HPow.hPow (β := ℕ) (a.sqrt + 1) 2
⊢ (↑a : ℝ) < HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1) 2

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
norm_cast : 0 ≤ a.sqrt + 1
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ a < HPow.hPow (β := ℕ) (a.sqrt + 1) 2

Tactic:
Nat.lt_succ_sqrt' a

Premises used: Nat.lt_succ_sqrt'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ a < HPow.hPow (β := ℕ) (a.sqrt + 1) 2

Tactic:
exact Nat.lt_succ_sqrt' a

Premises used: Nat.lt_succ_sqrt'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ 0 ≤ a.sqrt + 1

Tactic:
Nat.le_add_left 0 (Nat.sqrt a + 1)

Premises used: Nat.le_add_left, Nat.sqrt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ 0 ≤ a.sqrt + 1

Tactic:
exact Nat.le_add_left 0 (Nat.sqrt a + 1)

Premises used: Nat.le_add_left, Nat.sqrt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ √(↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1

Tactic:
real_sqrt_lt_nat_sqrt_succ.le

Premises used: Real.real_sqrt_lt_nat_sqrt_succ, LT.lt.le
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
rw : (↑(↑a.sqrt : ℤ) : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑(↑a.sqrt : ℤ) : ℝ) 1
⊢ ⌊√(↑a : ℝ)⌋ = (↑a.sqrt : ℤ)

Tactic:
rw [Int.floor_eq_iff]

Premises used: Int.floor_eq_iff
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ (↑(↑a.sqrt : ℤ) : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑(↑a.sqrt : ℤ) : ℝ) 1

Tactic:
⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Premises used: Real.real_sqrt_lt_nat_sqrt_succ, And.intro, Real.nat_sqrt_le_real_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ (↑(↑a.sqrt : ℤ) : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑(↑a.sqrt : ℤ) : ℝ) 1

Tactic:
exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
rw : (↑a.sqrt : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1
⊢ ⌊√(↑a : ℝ)⌋₊ = a.sqrt

Tactic:
rw [Nat.floor_eq_iff (sqrt_nonneg a)]

Premises used: Nat.floor_eq_iff, Nat.cast, Real.sqrt_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ (↑a.sqrt : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1

Tactic:
⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Premises used: Real.real_sqrt_lt_nat_sqrt_succ, And.intro, Real.nat_sqrt_le_real_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
a : ℕ
⊢ (↑a.sqrt : ℝ) ≤ √(↑a : ℝ) ∧ √(↑a : ℝ) < HAdd.hAdd (α := ℝ) (↑a.sqrt : ℝ) 1

Tactic:
exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩
-- Module: Mathlib.Data.Real.Sqrt
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
linarith₃ : 1 + x / 2 < 0 → -1 + (-1 - x) + (HMul.hMul (α := ℝ) 2 1 + 1 * x - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ 1 + x / 2

Tactic:
linarith
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : -1 ≤ x
refine : 1 + x ≤ HPow.hPow (β := ℕ) (1 + x / 2) 2
⊢ √(1 + x) ≤ 1 + x / 2

Tactic:
refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩

Premises used: Iff.mpr, Real.sqrt_le_iff, And.intro
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : -1 ≤ x
⊢ 1 + x ≤ 1 + x + HPow.hPow (β := ℕ) (x / 2) 2

Tactic:
le_add_of_nonneg_right <| sq_nonneg _

Premises used: le_add_of_nonneg_right, sq_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : -1 ≤ x
⊢ 1 + x + HPow.hPow (β := ℕ) (x / 2) 2 = HPow.hPow (β := ℕ) (1 + x / 2) 2

Tactic:
ring
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : -1 ≤ x
calc : 1 + x + HPow.hPow (β := ℕ) (x / 2) 2 = HPow.hPow (β := ℕ) (1 + x / 2) 2
⊢ 1 + x ≤ HPow.hPow (β := ℕ) (1 + x / 2) 2

Tactic:
calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = _ := by ring

Premises used: HDiv.hDiv, le_add_of_nonneg_right, sq_nonneg, OfNat.ofNat
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ (↑((NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) (∏ x_1 ∈ s, (toNNReal ∘ x) x_1)) : ℝ) =
    (↑(∏ x_1 ∈ s, (NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) ((toNNReal ∘ x) x_1)) : ℝ)

Tactic:
congr_arg NNReal.toReal <| map_prod NNReal.sqrtHom (Real.toNNReal ∘ x) s

Premises used: Function.comp, map_prod, congr_arg, NNReal.sqrtHom, NNReal.toReal, Real.toNNReal
-- Module: Mathlib.Data.Real.Sqrt
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)) : ℝ)
h₁ : ∏ i ∈ s, √(x i) = (↑(∏ x_1 ∈ s, (NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) ((toNNReal ∘ x) x_1)) : ℝ)
⊢ √(∏ i ∈ s, x i) = ∏ i ∈ s, √(x i)

Tactic:
convert! congr_arg NNReal.toReal <| map_prod NNReal.sqrtHom (Real.toNNReal ∘ x) s

Premises used: Function.comp, map_prod, congr_arg, NNReal.sqrtHom, NNReal.toReal, Real.toNNReal
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = (↑((NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) (∏ x_1 ∈ s, (toNNReal ∘ x) x_1)) : ℝ)

Tactic:
simp +contextual [-map_prod, NNReal.sqrtHom, hx]

Premises used: map_prod, NNReal.sqrtHom
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ ∏ i ∈ s, √(x i) = (↑(∏ x_1 ∈ s, (NNReal.sqrtHom : (a : ℝ≥0) → ℝ≥0) ((toNNReal ∘ x) x_1)) : ℝ)

Tactic:
simp +contextual [-map_prod, NNReal.sqrtHom, hx]

Premises used: map_prod, NNReal.sqrtHom
-- Module: Mathlib.Data.Real.Sqrt
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
x : ℝ
h : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (x : α) ↦ √(f x)) l (𝓝 √x)

Tactic:
(continuous_sqrt.tendsto _).comp h

Premises used: Real.continuous_sqrt, Continuous.tendsto, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Data.Real.Sqrt
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
x : α
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : α) ↦ √(f x)) s x

Tactic:
h.sqrt

Premises used: ContinuousWithinAt, Filter.Tendsto.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
x : α
h : ContinuousAt f x
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ √(f x)) x

Tactic:
h.sqrt

Premises used: ContinuousAt, Filter.Tendsto.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (x : α) ↦ √(f x)) s

Tactic:
fun x hx => (h x hx).sqrt

Premises used: ContinuousWithinAt.sqrt, ContinuousOn
-- Module: Mathlib.Data.Real.Sqrt
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : α) ↦ √(f x)

Tactic:
continuous_sqrt.comp h

Premises used: Continuous.comp, Real.continuous_sqrt, NNReal.toReal
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_2
s : Finset ι
f g : ι → ℝ≥0
⊢ ∑ i ∈ s, f i * g i ≤
    HMul.hMul (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2))
      ((sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℕ) (g i) 2))

Tactic:
(le_sqrt_iff_sq_le.2 <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul _ _

Premises used: Iff.mpr, LE.le.trans_eq, NNReal.le_sqrt_iff_sq_le, NNReal.sqrt_mul, Finset.sum_mul_sq_le_sq_mul_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_2
s : Finset ι
f g : ι → ℝ≥0
⊢ ∑ i ∈ s,
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (f i) : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (g i) : ℝ≥0) ≤
    HMul.hMul (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i ∈ s, f i)) ((sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i ∈ s, g i))

Tactic:
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ sqrt (f x)) (fun x ↦ sqrt (g x))

Premises used: NNReal.sqrt, NNReal.sum_mul_le_sqrt_mul_sqrt, DFunLike.coe
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_2
s : Finset ι
f g : ι → ℝ
x : ι
h : x ∈ s
⊢ 0 ≤ HPow.hPow (β := ℕ) (f x) 2

Tactic:
positivity
-- Module: Mathlib.Data.Real.Sqrt
Goal:
ι : Type u_2
f g : ι → ℝ
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
⊢ ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Tactic:
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))

Premises used: Real.sum_mul_le_sqrt_mul_sqrt, Real.sqrt
-- Module: Mathlib.Data.Real.Star
Goal:
⊢ TrivialStar ℝ

Tactic:
⟨fun _ => rfl⟩

Premises used: TrivialStar.mk, rfl
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
r : ℝ
⊢ 0 ≤ r ↔ ∃ (s : ℝ), r = star s * s

Tactic:
⟨fun hr => ⟨√r, (mul_self_sqrt hr).symm⟩, ?_⟩

Premises used: Real.mul_self_sqrt, Iff.intro, Exists.intro, Real.sqrt, Eq.symm
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
r : ℝ
refine : (∃ (s : ℝ), r = star s * s) → 0 ≤ r
⊢ 0 ≤ r ↔ ∃ (s : ℝ), r = star s * s

Tactic:
refine ⟨fun hr => ⟨√r, (mul_self_sqrt hr).symm⟩, ?_⟩
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
s : ℝ
⊢ 0 ≤ star s * s

Tactic:
mul_self_nonneg s

Premises used: mul_self_nonneg
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
s : ℝ
⊢ 0 ≤ star s * s

Tactic:
exact mul_self_nonneg s

Premises used: mul_self_nonneg
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
⊢ StarOrderedRing ℝ≥0

Tactic:
.of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩

Premises used: StarOrderedRing.of_le_iff, Iff.intro
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
refine_1 : ∀ (x y : ℝ≥0) (h : x ≤ y), ∃ (s : ℝ≥0), y = x + star s * s
refine_2 : ∀ (x y : ℝ≥0), (∃ (s : ℝ≥0), y = x + star s * s) → x ≤ y
⊢ StarOrderedRing ℝ≥0

Tactic:
refine .of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x y : ℝ≥0
h : x ≤ y
refine_1 : ∀ (d : ℝ≥0) (h : x ≤ x + d), ∃ (s : ℝ≥0), x + d = x + star s * s
⊢ ∃ (s : ℝ≥0), y = x + star s * s

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x d : ℝ≥0
h : x ≤ x + d
⊢ ∃ (s : ℝ≥0), x + d = x + star s * s

Tactic:
⟨sqrt d, ?_⟩

Premises used: NNReal.sqrt, Exists.intro, DFunLike.coe
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x d : ℝ≥0
h : x ≤ x + d
refine_1 :
  x + d =
    x + HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (star ((sqrt : (a : ℝ≥0) → ℝ≥0) d) : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) d : ℝ≥0)
⊢ ∃ (s : ℝ≥0), x + d = x + star s * s

Tactic:
refine ⟨sqrt d, ?_⟩
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x d : ℝ≥0
h : x ≤ x + d
⊢ x + d =
    x + HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (star ((sqrt : (a : ℝ≥0) → ℝ≥0) d) : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) d : ℝ≥0)

Tactic:
simp only [star_trivial, mul_self_sqrt]

Premises used: TrivialStar.star_trivial, NNReal.mul_self_sqrt
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x p : ℝ≥0
⊢ x ≤ x + star p * p

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Real.StarOrdered
Goal:
x p : ℝ≥0
⊢ x ≤ x + star p * p

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
N : Set X
⊢ U.IsCover ∅ N

Tactic:
simp [IsCover]

Premises used: SetRel.IsCover
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
s : Set X
⊢ U.IsCover s ∅ ↔ s = ∅

Tactic:
simp [IsCover, eq_empty_iff_forall_notMem]

Premises used: SetRel.IsCover, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
s N : Set X
hsN : U.IsCover s N
hs : s.Nonempty
⊢ N.Nonempty

Tactic:
let ⟨_x, hx⟩ := hs; let ⟨y, hy, _⟩ := hsN hx; ⟨y, hy⟩

Premises used: _private.0.SetRel.IsCover.nonempty.match_2, _private.0.SetRel.IsCover.nonempty.match_1, Set.Nonempty, Exists.intro
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
inst : U.IsRefl
s : Set X
⊢ U.IsCover s s

Tactic:
fun a ha ↦ ⟨a, ha, U.rfl⟩

Premises used: SetRel.rfl, SetRel.IsCover, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
inst : U.IsRefl
s : Set X
⊢ U.IsCover s s

Tactic:
refl U s

Premises used: SetRel.IsCover.refl
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
s N : Set X
⊢ IsCover univ s N ↔ s.Nonempty → N.Nonempty

Tactic:
simp [IsCover, Set.Nonempty]

Premises used: Set.Nonempty, SetRel.IsCover
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
s N₁ N₂ : Set X
hN : N₁ ⊆ N₂
h₁ : U.IsCover s N₁
⊢ U.IsCover s N₂

Tactic:
fun _x hx ↦ let ⟨y, hy, hxy⟩ := h₁ hx; ⟨y, hN hy, hxy⟩

Premises used: Membership.mem, Exists, Prod.mk, _private.0.SetRel.IsCover.nonempty.match_1, And, SetRel.IsCover, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
s t N : Set X
hst : s ⊆ t
ht : U.IsCover t N
⊢ U.IsCover s N

Tactic:
fun _x hx ↦ ht <| hst hx

Premises used: SetRel.IsCover
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U V : SetRel X X
s N : Set X
hUV : U ⊆ V
hU : U.IsCover s N
⊢ V.IsCover s N

Tactic:
fun _x hx ↦ let ⟨y, hy, hxy⟩ := hU hx; ⟨y, hy, hUV hxy⟩

Premises used: Membership.mem, Exists, Prod.mk, _private.0.SetRel.IsCover.nonempty.match_1, And, SetRel.IsCover, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
U : SetRel X X
s t N₁ N₂ : Set X
hs : U.IsCover s N₁
ht : U.IsCover t N₂
⊢ U.IsCover (s ∪ t) (N₁ ∪ N₂)

Tactic:
fun
  | _x, .inl hx => let ⟨y, hy, hxy⟩ := hs hx; ⟨y, .inl hy, hxy⟩
  | _x, .inr hx => let ⟨y, hy, hxy⟩ := ht hx; ⟨y, .inr hy, hxy⟩

Premises used: _private.0.SetRel.IsCover.union.match_1, Membership.mem, Exists, Prod.mk, _private.0.SetRel.IsCover.nonempty.match_1, And, SetRel.IsCover, And.intro, Exists.intro, Or.inl, Union.union, Or.inr
-- Module: Mathlib.Data.Rel.Cover
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
by_contra! : ∀ (h : ∀ (y : X) (_ : y ∈ N), ¬(x, y) ∈ U), False
⊢ ∃ (y : X), y ∈ N ∧ (x, y) ∈ U

Tactic:
by_contra! h
-- Module: Mathlib.Data.Rel.Cover
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
h : ∀ (y : X) (_ : y ∈ N), ¬(x, y) ∈ U
⊢ insert x N ⊆ s

Tactic:
simp [insert_subset_iff, hx, hN.1.1]

Premises used: Set.insert_subset_iff, And.left
-- Module: Mathlib.Data.Rel.Cover
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
h : ∀ (y : X) (_ : y ∈ N), ¬(x, y) ∈ U
⊢ False

Tactic:
simpa [U.rfl] using h _ <| hN.2 (y := insert x N) ⟨by simp [insert_subset_iff, hx, hN.1.1],
    hN.1.2.insert fun y hy hxy ↦ (h y hy hxy).elim⟩ (subset_insert _ _) (mem_insert _ _)

Premises used: False.elim, SetRel.IsSeparated.insert, SetRel.rfl, And.right, And.left, And.intro, Set.mem_insert, Set.subset_insert
-- Module: Mathlib.Data.Rel.Cover
Goal:
X : Type u_1
s N : Set X
⊢ IsCover SetRel.id s N ↔ s ⊆ N

Tactic:
simp [IsCover, subset_def]

Premises used: Set.subset_def, SetRel.IsCover
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
⊢ R.IsSeparated ∅

Tactic:
pairwise_empty _

Premises used: Set.pairwise_empty, SetRel.IsSeparated
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
x : X
⊢ R.IsSeparated {x}

Tactic:
pairwise_singleton ..

Premises used: SetRel.IsSeparated, Set.pairwise_singleton
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
hs : s.Subsingleton
⊢ R.IsSeparated s

Tactic:
hs.pairwise _

Premises used: SetRel.IsSeparated, Set.Subsingleton.pairwise
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R S : SetRel X X
s : Set X
hUV : R ⊆ S
hs : S.IsSeparated s
⊢ R.IsSeparated s

Tactic:
hs.mono' fun _x _y hxy h ↦ hxy <| hUV h

Premises used: SetRel.IsSeparated, Set.Pairwise.mono'
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s t : Set X
hst : s ⊆ t
ht : R.IsSeparated t
⊢ R.IsSeparated s

Tactic:
ht.mono hst

Premises used: Set.Pairwise.mono, SetRel.IsSeparated
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
x : X
⊢ R.IsSeparated (insert x s) ↔
    R.IsSeparated s ∧ (∀ (y : X), y ∈ s → (x, y) ∈ R → x = y) ∧ ∀ (y : X), y ∈ s → (y, x) ∈ R → x = y

Tactic:
simp [IsSeparated, pairwise_insert, not_imp_comm (a := _ = _), -not_and, forall_and]

Premises used: not_imp_comm, SetRel.IsSeparated, Set.pairwise_insert, not_and, forall_and
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
x : X
inst : R.IsSymm
⊢ R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y

Tactic:
simpa [not_imp_not, IsSeparated] using pairwise_insert_of_symmetric fun _ _ ↦ mt R.symm

Premises used: mt, SetRel.symm, SetRel.IsSeparated, Set.pairwise_insert_of_symmetric, not_imp_not
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
x : X
inst : R.IsSymm
hx : ¬x ∈ s
⊢ R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → ¬(x, y) ∈ R

Tactic:
pairwise_insert_of_symmetric_of_notMem (fun _ _ ↦ mt R.symm) hx

Premises used: mt, SetRel.symm, Set.pairwise_insert_of_symmetric_of_notMem, SetRel.IsSeparated
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
x : X
hs : R.IsSeparated s
h : ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y
h' : ∀ (y : X), y ∈ s → (y, x) ∈ R → x = y
⊢ R.IsSeparated (insert x s)

Tactic:
isSeparated_insert'.2 ⟨hs, h, h'⟩

Premises used: Iff.mpr, SetRel.isSeparated_insert', And.intro
-- Module: Mathlib.Data.Rel.Separated
Goal:
X : Type u_1
R : SetRel X X
s : Set X
x : X
inst : R.IsSymm
hs : R.IsSeparated s
h : ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y
⊢ R.IsSeparated (insert x s)

Tactic:
isSeparated_insert.2 ⟨hs, h⟩

Premises used: Iff.mpr, And.intro, SetRel.isSeparated_insert
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
a : α
b : β
⊢ (b, a) ∈ R.inv ↔ (a, b) ∈ R

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, SetRel.inv, setOf, Set.preimage, Prod.swap
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.inv.inv = R

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R₁ R₂ : SetRel α β
h : R₁ ⊆ R₂
⊢ R₁.inv ⊆ R₂.inv

Tactic:
fun (_a, _b) hab ↦ h hab

Premises used: _private.0.SetRel.inv_mono.match_1, SetRel.inv, Membership.mem, Set.Subset
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := SetRel β α) (inv ∅) ∅

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := SetRel β α) (inv Set.univ) Set.univ

Tactic:
rfl

Premises used: Set.Mem, Set.univ, SetRel.inv, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
a : α
⊢ a ∈ R.dom ↔ ∃ (b : β), (a, b) ∈ R

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.dom