awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
⊢ 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⟫)

Tactic:
classical exact hv.inner_left_right_finset

Premises used: Orthonormal.inner_left_right_finset
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
⊢ 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⟫)

Tactic:
have h₂ :
    (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) = (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫ : 𝕜) := by
    classical exact hv.inner_left_right_finset
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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⟫)
z : 𝕜
simp : (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖z‖ : 𝕜) 2) = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
simp only [mul_conj]

Premises used: RCLike.mul_conj
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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⟫)
z : 𝕜
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HPow.hPow (β := ℕ) ‖z‖ 2 = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖z‖ : 𝕜) 2) = HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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⟫)
⊢ ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
have h₃ : ∀ z : 𝕜, re (z * conj z) = ‖z‖ ^ 2 := by
    intro z
    simp only [mul_conj]
    norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
hbf :
  HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
rw : 0 ≤ HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [← sub_nonneg, ← hbf]

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
hbf :
  HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2

Tactic:
simp only [norm_nonneg, pow_nonneg]

Premises used: pow_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
suffices :
  HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
suffices hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 by
    rw [← sub_nonneg, ← hbf]
    simp only [norm_nonneg, pow_nonneg]
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
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
⊢ HPow.hPow (β := ℕ) ‖x - ∑ 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]

Premises used: sub_add, norm_sub_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
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 : ℝ)
⊢ 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:
simp only [@InnerProductSpace.norm_sq_eq_re_inner 𝕜 E, inner_sum, sum_inner]

Premises used: inner_sum, sum_inner, InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
simp :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (∑ x_1 ∈ s, ⟪v x_1, x⟫ * ⟪x, v x_1⟫) : ℝ)
    (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 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 : ℝ)

Tactic:
simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ← mul_assoc, h₂,
    add_sub_cancel_right, sub_right_inj]

Premises used: sub_right_inj, mul_assoc, two_mul, inner_smul_right, add_sub_cancel_right, inner_conj_symm, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
⊢ 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 [map_sum, ← inner_conj_symm x, ← h₃]

Premises used: map_sum, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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

Tactic:
tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x

Premises used: tsum_le_of_sum_le', Orthonormal.sum_inner_products_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
refine : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ∑' (i : ι), HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x

Premises used: tsum_le_of_sum_le', Orthonormal.sum_inner_products_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simp only [norm_nonneg, pow_nonneg]

Premises used: pow_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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 :
  HasSum (α := ℝ) (fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
    (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2

Tactic:
use ⨆ s : Finset ι, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2

Premises used: Finset
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
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)
⊢ HasSum (α := ℝ) (fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
    (⨆ (s : Finset ι), ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)

Tactic:
apply hasSum_of_isLUB_of_nonneg

Premises used: hasSum_of_isLUB_of_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
b : ι
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖⟪v b, x⟫‖ 2

Tactic:
simp only [norm_nonneg, pow_nonneg]

Premises used: pow_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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)

Tactic:
isLUB_ciSup ?_

Premises used: isLUB_ciSup
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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 : BddAbove (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)
⊢ 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:
refine isLUB_ciSup ?_

Premises used: isLUB_ciSup
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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 :
  Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2))
    (HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ BddAbove (α := ℝ) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2)

Tactic:
use ‖x‖ ^ 2
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 : ℝ)) s ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
hv.sum_inner_products_le x

Premises used: Orthonormal.sum_inner_products_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
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
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 : ℝ)) s ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
exact hv.sum_inner_products_le x

Premises used: Orthonormal.sum_inner_products_le
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : PiLp 2 f
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (∑ i : ι, ⟪x.ofLp i, x.ofLp i⟫)

Tactic:
simp only [PiLp.norm_sq_eq_of_L2, map_sum, ← norm_sq_eq_re_inner]

Premises used: PiLp.norm_sq_eq_of_L2, map_sum, InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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) :
      𝕜)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑ i : ι, ⟪y.ofLp i, x.ofLp i⟫) : 𝕜) (∑ i : ι, ⟪x.ofLp i, y.ofLp i⟫ : 𝕜)

Tactic:
unfold inner

Premises used: Inner.inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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))
⊢ 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:
rw [map_sum]

Premises used: map_sum
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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) :
          𝕜)
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
z : ι
⊢ Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ :
              Inner.{u_3, u_8} 𝕜 (f z)).1
          (y.ofLp z) (x.ofLp z)) :
      𝕜)
    ((@InnerProductSpace.toInner _ _ inst NormedAddCommGroup.toSeminormedAddCommGroup _ : Inner.{u_3, u_8} 𝕜 (f z)).1
        (x.ofLp z) (y.ofLp z) :
      𝕜)

Tactic:
apply inner_conj_symm

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 z : PiLp 2 f
⊢ ∑ i : ι, ⟪x.ofLp i + y.ofLp i, z.ofLp i⟫ =
    HAdd.hAdd (α := 𝕜) (∑ i : ι, ⟪x.ofLp i, z.ofLp i⟫) (∑ i : ι, ⟪y.ofLp i, z.ofLp i⟫)

Tactic:
simp only [inner_add_left, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
r : 𝕜
⊢ ∑ i : ι, ⟪r • x.ofLp i, y.ofLp i⟫ =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (∑ i : ι, ⟪x.ofLp i, y.ofLp i⟫ : 𝕜)

Tactic:
simp only [Finset.mul_sum, inner_smul_left]

Premises used: Finset.mul_sum, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
ι : Type u_7
inst_1 : Fintype ι
f : ι → Type u_8
inst_2 : (i : ι) → NormedAddCommGroup (f i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_8} 𝕜 (f i)
x y : PiLp 2 f
⊢ ⟪x, y⟫ = ∑ i : ι, ⟪x.ofLp i, y.ofLp i⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x : EuclideanSpace 𝕜 n
⊢ ‖x‖₊ = (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : n, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)

Tactic:
PiLp.nnnorm_eq_of_L2 x

Premises used: PiLp.nnnorm_eq_of_L2, setOf
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x : EuclideanSpace 𝕜 n
⊢ ‖x‖ = √(∑ i : n, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)

Tactic:
simpa only [Real.coe_sqrt, NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq

Premises used: NNReal.coe_sum, congr_arg, EuclideanSpace.nnnorm_eq, Real.coe_sqrt, NNReal.toReal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x : EuclideanSpace 𝕜 n
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ∑ i : n, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2

Tactic:
PiLp.norm_sq_eq_of_L2 _ x

Premises used: setOf, PiLp.norm_sq_eq_of_L2
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
x : EuclideanSpace ℝ n
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2

Tactic:
simp [EuclideanSpace.norm_sq_eq]

Premises used: EuclideanSpace.norm_sq_eq
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x y : EuclideanSpace 𝕜 n
⊢ dist x y = √(∑ i : n, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2)

Tactic:
PiLp.dist_eq_of_L2 x y

Premises used: setOf, PiLp.dist_eq_of_L2
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x y : EuclideanSpace 𝕜 n
⊢ HPow.hPow (β := ℕ) (dist x y) 2 = ∑ i : n, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2

Tactic:
PiLp.dist_sq_eq_of_L2 x y

Premises used: setOf, PiLp.dist_sq_eq_of_L2
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x y : EuclideanSpace 𝕜 n
⊢ nndist x y = (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : n, HPow.hPow (β := ℕ) (nndist (x.ofLp i) (y.ofLp i)) 2)

Tactic:
PiLp.nndist_eq_of_L2 x y

Premises used: setOf, PiLp.nndist_eq_of_L2
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
inst : RCLike 𝕜
n : Type u_8
inst_1 : Fintype n
x y : EuclideanSpace 𝕜 n
⊢ edist x y = HPow.hPow (α := ℝ≥0∞) (∑ i : n, HPow.hPow (β := ℕ) (edist (x.ofLp i) (y.ofLp i)) 2) (1 / 2)

Tactic:
PiLp.edist_eq_of_L2 x y

Premises used: setOf, PiLp.edist_eq_of_L2