awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫)
h₃ :
  ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 -
    (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, ∑ i ∈ s, ⟪v i, x⟫ • v i⟫ : ℝ) -
      HPow.hPow (β := ℕ) (Norm.norm.{u_2} (E := E) (∑ i ∈ s, ⟪v i, x⟫ • v i)) 2) =
  HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
Tactic: rw [@norm_sub_sq 𝕜, sub_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫)
h₃ :
  ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 -
      (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, ∑ i ∈ s, ⟪v i, x⟫ • v i⟫ : ℝ) -
        HPow.hPow (β := ℕ) (Norm.norm.{u_2} (E := E) (∑ i ∈ s, ⟪v i, x⟫ • v i)) 2) =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
have simp : HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
    (HSub.hSub (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) (∑ i ∈ s, ⟪x, ⟪v i, x⟫ • v i⟫) : ℝ))
      ((re : (a : 𝕜) → ℝ) (∑ x_1 ∈ s, ∑ i ∈ s, ⟪⟪v i, x⟫ • v i, ⟪v x_1, x⟫ • v x_1⟫) : ℝ)) =
  HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 : ℝ)
Tactic: simp only [@InnerProductSpace.norm_sq_eq_re_inner 𝕜 E, inner_sum, sum_inner]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫)
h₃ :
  ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HSub.hSub (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) (∑ i ∈ s, ⟪x, ⟪v i, x⟫ • v i⟫) : ℝ))
        ((re : (a : 𝕜) → ℝ) (∑ x_1 ∈ s, ∑ i ∈ s, ⟪⟪v i, x⟫ • v i, ⟪v x_1, x⟫ • v x_1⟫) : ℝ)) =
    HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 : ℝ)
have simp : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (∑ x_1 ∈ s, ⟪v x_1, x⟫ * ⟪x, v x_1⟫) : ℝ) (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 : ℝ)
Tactic: simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ← mul_assoc, h₂,
    add_sub_cancel_right, sub_right_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∑' (i : ι), HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have refine : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
have h : HasSum (α := ℝ) (fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
  (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
Tactic: use ⨆ s : Finset ι, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ HasSum (α := ℝ) (fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
    (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
have h : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
Tactic: apply hasSum_of_isLUB_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
h : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
⊢ HasSum (α := ℝ) (fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
    (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
have h₁ : IsLUB (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
  (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
Tactic: apply hasSum_of_isLUB_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
    (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
have h : BddAbove (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
Tactic: refine isLUB_ciSup ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ BddAbove (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2))
  (HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: use ‖x‖ ^ 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
ι : Type u_7
inst_7 : Fintype ι
f : ι → Type u_8
inst_8 : (i : ι) → NormedAddCommGroup (f i)
inst_9 : (i : ι) → InnerProductSpace.{u_3, u_8} 𝕜 (f i)
x y : PiLp 2 f
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑ i : ι, ⟪y.ofLp i, x.ofLp i⟫) : 𝕜) (∑ i : ι, ⟪x.ofLp i, y.ofLp i⟫ : 𝕜)
have unfold : Eq (α := 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
      (∑ i : ι,
        (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f i)).1
          (y.ofLp i) (x.ofLp i)) :
    𝕜)
  (∑ i : ι,
      (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f i)).1
        (x.ofLp i) (y.ofLp i) :
    𝕜)
Tactic: unfold inner
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
ι : Type u_7
inst_7 : Fintype ι
f : ι → Type u_8
inst_8 : (i : ι) → NormedAddCommGroup (f i)
inst_9 : (i : ι) → InnerProductSpace.{u_3, u_8} 𝕜 (f i)
x y : PiLp 2 f
⊢ Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        (∑ i : ι,
          (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
                Inner.{u_3, u_8} 𝕜 (f i)).1
            (y.ofLp i) (x.ofLp i)) :
      𝕜)
    (∑ i : ι,
        (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f i)).1
          (x.ofLp i) (y.ofLp i) :
      𝕜)
have rw : Eq.{u_3 + 1} (α := 𝕜)
  (∑ x_1 : ι,
    (starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
      ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
            Inner.{u_3, u_8} 𝕜 (f x_1)).1
        (y.ofLp x_1) (x.ofLp x_1)))
  (∑ i : ι,
    (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f i)).1
      (x.ofLp i) (y.ofLp i))
Tactic: rw [map_sum]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
ι : Type u_7
inst_7 : Fintype ι
f : ι → Type u_8
inst_8 : (i : ι) → NormedAddCommGroup (f i)
inst_9 : (i : ι) → InnerProductSpace.{u_3, u_8} 𝕜 (f i)
x y : PiLp 2 f
⊢ Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
      (starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
              Inner.{u_3, u_8} 𝕜 (f x_1)).1
          (y.ofLp x_1) (x.ofLp x_1)))
    (∑ i : ι,
      (@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f i)).1
        (x.ofLp i) (y.ofLp i))
have apply : ∀ (x_1 : ι),
  Membership.mem (γ := Finset ι) Finset.univ x_1 →
    Eq (α := 𝕜)
      ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
          ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
                Inner.{u_3, u_8} 𝕜 (f x_1)).1
            (y.ofLp x_1) (x.ofLp x_1)) :
        𝕜)
      ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
              Inner.{u_3, u_8} 𝕜 (f x_1)).1
          (x.ofLp x_1) (y.ofLp x_1) :
        𝕜)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2}
have h : ∀ (x : EuclideanSpace ℝ n),
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
Tactic: have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have h₂ : Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have h₃ : ‖x‖ < r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ < r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have h₄ : √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) < r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ < r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have h₅ : √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) < r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ < r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₅ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
have h₆ : √(∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2) < r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2}
have h : ∀ (x : EuclideanSpace ℝ n),
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
have h₂ : Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
have h₃ : ‖x‖ ≤ r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ ≤ r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
have h₄ : √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) ≤ r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ ≤ r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
have h₅ : √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) ≤ r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ ≤ r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₅ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
have h₆ : √(∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2) ≤ r ↔
  ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
Tactic: simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2}
have h : ∀ (x : EuclideanSpace ℝ n),
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2} x
have this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
Tactic: have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _