awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ Eq.{u_3 + 1} (α := 𝕜) ((((b.toBasis.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
    (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i : (fun (x : ι) ↦ 𝕜) i)

Tactic:
simp [← Basis.equivFun_apply]

Premises used: Module.Basis.equivFun_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
simp_rw :
  ∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
        ((((b.toBasis.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) x_1 : 𝕜) ((b.toBasis : (a : ι) → E) x_1 : E) =
    x
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i) ((b : (a : ι) → E) i : E) =
    x

Tactic:
simp_rw [← b.coe_toBasis_repr_apply, ← b.coe_toBasis]

Premises used: OrthonormalBasis.coe_toBasis, OrthonormalBasis.coe_toBasis_repr_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
        ((((b.toBasis.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) x_1 : 𝕜) ((b.toBasis : (a : ι) → E) x_1 : E) =
    x

Tactic:
b.toBasis.sum_repr x

Premises used: Module.Basis.sum_repr, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
        ((((b.toBasis.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) x_1 : 𝕜) ((b.toBasis : (a : ι) → E) x_1 : E) =
    x

Tactic:
exact b.toBasis.sum_repr x

Premises used: Module.Basis.sum_repr, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
nth_rw :
  Eq.{u_4 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E))
    (∑ i : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i) ((b : (a : ι) → E) i : E))
⊢ ∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E) = x

Tactic:
nth_rw 2 [← (b.sum_repr x)]

Premises used: OrthonormalBasis.sum_repr
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E))
    (∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E) (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1)
        ((b : (a : ι) → E) x_1 : E))
⊢ Eq.{u_4 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E))
    (∑ i : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i) ((b : (a : ι) → E) i : E))

Tactic:
simp_rw [b.repr_apply_apply x]

Premises used: OrthonormalBasis.repr_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : EuclideanSpace 𝕜 ι
⊢ Eq.{u_4 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) (v.ofLp i) ((b : (a : ι) → E) i : E) : E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) v : E)

Tactic:
simpa using (b.toBasis.equivFun_symm_apply v).symm

Premises used: Module.Basis.equivFun_symm_apply, Eq.symm, WithLp.ofLp, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
⊢ Eq.{u_3 + 1} (α := 𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
        (∑ i : ι,
          HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) i) ((b : (a : ι) → E) i : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)

Tactic:
have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
        (∑ i : ι,
          HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) i) ((b : (a : ι) → E) i : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
⊢ Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)

Tactic:
rw [map_sum] at this

Premises used: map_sum
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
⊢ Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)

Tactic:
this
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
h :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ x_1 →
      ⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, y⟫ =
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E))
⊢ ∑ i : ι, ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪x, y⟫

Tactic:
convert! this
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_2 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_2) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_2) ((b : (a : ι) → E) x_2 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
x_1 : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ x_1
h :
  ⟪(b : (a : ι) → E) x_1, y⟫ * ⟪x, (b : (a : ι) → E) x_1⟫ =
    HSMul.hSMul (β := 𝕜) ⟪(b : (a : ι) → E) x_1, y⟫
      ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) x_1 : E) : 𝕜)
⊢ ⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E))

Tactic:
rw [map_smul, b.repr_apply_apply, mul_comm]

Premises used: OrthonormalBasis.repr_apply_apply, mul_comm, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_2 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_2) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_2) ((b : (a : ι) → E) x_2 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
⊢ ⟪(b : (a : ι) → E) x_1, y⟫ * ⟪x, (b : (a : ι) → E) x_1⟫ =
    HSMul.hSMul (β := 𝕜) ⟪(b : (a : ι) → E) x_1, y⟫
      ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) x_1 : E) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
rw :
  ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, (re : (a : 𝕜) → ℝ) (⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, x⟫))) 2
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [@norm_eq_sqrt_re_inner 𝕜, ← OrthonormalBasis.sum_inner_mul_inner b x x, map_sum]

Premises used: OrthonormalBasis.sum_inner_mul_inner, map_sum, norm_eq_sqrt_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
simp_rw :
  ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)) 2
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, (re : (a : 𝕜) → ℝ) (⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, x⟫))) 2

Tactic:
simp_rw [inner_mul_symm_re_eq_norm, norm_mul, ← inner_conj_symm x, starRingEnd_apply,
    norm_star, ← pow_two]

Premises used: norm_star, pow_two, norm_mul, starRingEnd_apply, inner_mul_symm_re_eq_norm, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
rw : LE.le (α := ℝ) 0 (∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)) 2

Tactic:
rw [Real.sq_sqrt]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
x_1 : ι
⊢ 0 x_1 ≤ HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ LE.le (α := ℝ) 0 (∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)

Tactic:
exact Fintype.sum_nonneg fun _ ↦ by positivity

Premises used: Fintype.sum_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
sum_sq_norm_inner_right b x

Premises used: OrthonormalBasis.sum_sq_norm_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h : ∀ (i : ι), HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
convert! sum_sq_norm_inner_right b x using 2 with i -

Premises used: OrthonormalBasis.sum_sq_norm_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
h :
  HPow.hPow (β := ℕ) (Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)) 2 =
    HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
h₁ h₂ : HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
⊢ HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2

Tactic:
rw [← inner_conj_symm, RCLike.norm_conj]

Premises used: RCLike.norm_conj, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
x : E
rw :
  Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2)
    (∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [← b.sum_sq_norm_inner_right]

Premises used: OrthonormalBasis.sum_sq_norm_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
x : E
⊢ Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2)
    (∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fintype ι
b : OrthonormalBasis ι ℝ E
x : E
simp_rw :
  Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ⟪x, (b : (a : ι) → E) i⟫ 2)
    (∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2)
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ⟪x, (b : (a : ι) → E) i⟫ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simp_rw [← b.sum_sq_inner_right, real_inner_comm]

Premises used: OrthonormalBasis.sum_sq_inner_right, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
rw : ‖x‖ = √(HPow.hPow (β := ℕ) ‖x‖ 2)
rw₁ rw₂ : ‖x‖ = ‖x‖
⊢ ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)

Tactic:
rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]

Premises used: OrthonormalBasis.sum_sq_norm_inner_right, Real.sqrt_sq
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
a :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → ‖⟪(b : (a : ι) → E) i, x⟫‖ ≤ ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
⊢ √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2) ≤
    √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2)

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ BddAbove (α := ℝ) (range fun (j : ι) ↦ ‖⟪(b : (a : ι) → E) j, x⟫‖)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖⟪(b : (a : ι) → E) i, x⟫‖ ≤ ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖

Tactic:
exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
simp :
  √(↑(Fintype.card ι) : ℝ) * √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
⊢ √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖

Tactic:
simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]

Premises used: Finset.card_univ, Nat.cast_nonneg, Real.sqrt_mul, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
e_a : √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) = ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
⊢ √(↑(Fintype.card ι) : ℝ) * √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
e_a : LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) = ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖

Tactic:
rw [Real.sqrt_sq]

Premises used: Real.sqrt_sq
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
e_a : IsEmpty ι → LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
e_a₁ : Nonempty ι → LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
⊢ LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h : IsEmpty ι
⊢ LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h : Nonempty ι
⊢ BddAbove (α := ℝ) (range fun (j : ι) ↦ ‖⟪(b : (a : ι) → E) j, x⟫‖)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h : Nonempty ι
⊢ 0 ≤ ‖⟪(b : (a : ι) → E) (Nonempty.some ⋯), x⟫‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h : Nonempty ι
⊢ LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)

Tactic:
exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)

Premises used: le_ciSup_of_le, inferInstance, Nonempty.some
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
calc : ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
calc₁ :
  √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2) ≤
    √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2)
calc₂ :
  √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
⊢ ‖x‖ ≤ √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖

Tactic:
calc ‖x‖
  _ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
  _ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
    gcongr with i
    exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
  _ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
    congr
    rw [Real.sqrt_sq]
    cases isEmpty_or_nonempty ι
    · simp
    · exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)

Premises used: Fintype.card
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
b : OrthonormalBasis.{u_1, u_3, u_4} ι 𝕜 ↥U
x : E
⊢ Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) x : ↥U)
    (∑ i : ι, HSMul.hSMul (β := ↥U) ⟪(↑((b : (a : ι) → ↥U) i) : E), x⟫ ((b : (a : ι) → ↥U) i : ↥U) : ↥U)

Tactic:
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
    (b.sum_repr (U.orthogonalProjection x)).symm

Premises used: OrthonormalBasis.repr_apply_apply, Submodule.orthogonalProjection, Submodule.inner_orthogonalProjection_eq_of_mem_left, OrthonormalBasis.sum_repr, Eq.symm, DFunLike.coe