awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
rw :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((b : (a : ι) → E) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
rw₁ :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v)
rw₂ rw₃ rw₄ :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := 𝕜) 1 ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → 𝕜) i)
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫

Tactic:
classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
  simp

Premises used: HilbertBasis.repr, LinearIsometryEquiv.inner_map_map, lp.inner_single_left, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw :
  ∀ (i j : ι), inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
⊢ Orthonormal.{u_2, u_3, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
rw : inner 𝕜 (E := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
⊢ inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0

Tactic:
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]

Premises used: Pi.single_apply, HilbertBasis.repr, LinearIsometryEquiv.inner_map_map, lp.inner_single_left, HilbertBasis.repr_self, lp.single_apply, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner 𝕜 (E := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw rw₁ rw₂ rw₃ :
  ∀ (i j : ι), inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
rw₄ : ∀ (i j : ι), inner 𝕜 (E := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
⊢ Orthonormal.{u_2, u_3, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)

Tactic:
classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]
  simp

Premises used: Pi.single_apply, lp.inner_single_left, orthonormal_iff_ite, lp.single_apply
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
H :
  Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)
rw :
  HasSum.{u_3, u_1} (α := E)
    (fun (b_1 : ι) ↦
      (((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
          ((fun (i : ι) ↦
              (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) :
                ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
            b_1) :
        E))
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) f : E)
⊢ HasSum.{u_3, u_1} (α := E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) f : E)

Tactic:
rw [H]
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
H :
  Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)
⊢ HasSum (fun (i : ι) ↦ lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)) f

Tactic:
have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
H :
  Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)
this : HasSum (fun (i : ι) ↦ lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)) f
⊢ HasSum.{u_3, u_1} (α := E)
    (fun (b_1 : ι) ↦
      (((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
          ((fun (i : ι) ↦
              (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) :
                ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
            b_1) :
        E))
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) f : E)

Tactic:
(↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this

Premises used: LinearIsometryEquiv.symm, HilbertBasis.repr, ContinuousLinearMap.hasSum, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
H :
  Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)
this : HasSum (fun (i : ι) ↦ lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)) f
⊢ HasSum.{u_3, u_1} (α := E)
    (fun (b_1 : ι) ↦
      (((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
          ((fun (i : ι) ↦
              (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) :
                ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
            b_1) :
        E))
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) f : E)

Tactic:
exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this

Premises used: LinearIsometryEquiv.symm, HilbertBasis.repr, ContinuousLinearMap.hasSum, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
suffices :
  Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)
⊢ HasSum.{u_3, u_1} (α := E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) f : E)

Tactic:
suffices H : (fun i : ι => f i • b i) = fun b_1 : ι => b.repr.symm.toContinuousLinearEquiv <|
      (fun i : ι => lp.single 2 i (f i) (E := (fun _ : ι => 𝕜))) b_1 by
    rw [H]
    have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
    exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  ∀ (i : ι),
    HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E) =
      ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
        ((fun (i : ι) ↦
            (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
          i)
⊢ Eq (α := (i : ι) → E)
    (fun (i : ι) ↦ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E))
    fun (b_1 : ι) ↦
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        b_1)

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
h :
  Eq (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
        (HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E)) :
      ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
        (((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
          ((fun (i : ι) ↦
              (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) :
                ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
            i)) :
      ↥(lp (fun (x : ι) ↦ 𝕜) 2))
⊢ HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E) =
    ((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      ((fun (i : ι) ↦
          (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
        i)

Tactic:
apply b.repr.injective

Premises used: HilbertBasis.repr, LinearIsometryEquiv.injective
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
⊢ NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
this : NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2) := inferInstance
⊢ lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i * 1) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)

Tactic:
have : lp.single (E := (fun _ : ι => 𝕜)) 2 i (f i * 1) = f i • lp.single 2 i 1 :=
    lp.single_smul (E := (fun _ : ι => 𝕜)) 2 i (f i) (1 : 𝕜)
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
this_1 : NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2) := inferInstance
this :
  lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i * 1) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
⊢ lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)

Tactic:
rw [mul_one] at this

Premises used: mul_one
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
this_1 : NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2) := inferInstance
this :
  lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
h :
  Eq (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
        ((fun (i : ι) ↦
            (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
          i)))
⊢ Eq (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
        (HSMul.hSMul (β := E) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) ((b : (a : ι) → E) i : E)) :
      ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
        (((↑b.repr.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
          ((fun (i : ι) ↦
              (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) :
                ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
            i)) :
      ↥(lp (fun (x : ι) ↦ 𝕜) 2))

Tactic:
rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]

Premises used: LinearIsometryEquiv.coe_toContinuousLinearEquiv, HilbertBasis.repr_self, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
this_1 : NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2) := inferInstance
this :
  lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
⊢ Eq (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
        ((fun (i : ι) ↦
            (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
          i)))

Tactic:
(b.repr.apply_symm_apply (lp.single 2 i (f i))).symm

Premises used: LinearIsometryEquiv.apply_symm_apply, lp.single, HilbertBasis.repr, OfNat.ofNat, Eq.symm, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun (x : ι) ↦ 𝕜) 2)
i : ι
this_1 : NormedSpace 𝕜 ↥(lp (fun (_i : ι) ↦ 𝕜) 2) := inferInstance
this :
  lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) =
    HSMul.hSMul (β := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
⊢ Eq (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
        ((fun (i : ι) ↦
            (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i ((↑f : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2)))
          i)))

Tactic:
exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm

Premises used: LinearIsometryEquiv.apply_symm_apply, lp.single, HilbertBasis.repr, OfNat.ofNat, Eq.symm, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum
    (fun (i : ι) ↦
      HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
    x

Tactic:
simpa using b.hasSum_repr_symm (b.repr x)

Premises used: HilbertBasis.repr, DFunLike.coe, HilbertBasis.hasSum_repr_symm
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x

Tactic:
mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)

Premises used: Set.Mem, setOf, HilbertBasis.hasSum_repr, Filter.Eventually.of_forall, closure, Set.sInter, mem_closure_of_tendsto
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
refine :
  ∀ (x_1 : Finset ι),
    ∑ b_1 ∈ x_1,
        (fun (i : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
              ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
              ((b : (a : ι) → E) i : E))
          b_1 ∈
      (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x

Tactic:
refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)

Premises used: HilbertBasis.hasSum_repr, Filter.Eventually.of_forall, mem_closure_of_tendsto
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
simp :
  Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (∑ x_1 ∈ s,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))
⊢ ∑ b_1 ∈ s,
      (fun (i : ι) ↦
          HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
            ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
            ((b : (a : ι) → E) i : E))
        b_1 ∈
    (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)

Tactic:
simp only [SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (∑ x_1 ∈ s,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))

Tactic:
sum_mem ?_

Premises used: sum_mem
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
refine :
  ∀ c ∈ s,
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) c) ((b : (a : ι) → E) c : E))
⊢ Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (∑ x_1 ∈ s,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))

Tactic:
refine sum_mem ?_

Premises used: sum_mem
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
      ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) i) ((b : (a : ι) → E) i : E))

Tactic:
smul_mem _ _ ?_

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
refine :
  Membership.mem.{u_3, u_3} (α := E) (γ := Submodule 𝕜 E)
    (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ((b : (a : ι) → E) i : E)
⊢ Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
      ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) i) ((b : (a : ι) → E) i : E))

Tactic:
refine smul_mem _ _ ?_

Premises used: Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Submodule 𝕜 E)
    (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ((b : (a : ι) → E) i : E)

Tactic:
subset_span ⟨i, rfl⟩

Premises used: Exists.intro, Submodule.subset_span, rfl