awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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
⊢ Orthonormal.{u_2, u_3, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)
have rw₄ : ∀ (i j : ι), inner 𝕜 (E := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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.{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)
have 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)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
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.{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)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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)
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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)
⊢ 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)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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 : ι
⊢ 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)
have 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))
Tactic: apply b.repr.injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
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
⊢ 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))
have 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)
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 : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
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)
⊢ 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))
have 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)
Tactic: rw [mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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))
    ((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))
have 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)))
Tactic: rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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)
⊢ 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)
have 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)
Tactic: classical
  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
  ext i
  apply b.repr.injective
  letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
  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 : 𝕜)
  rw [mul_one] at this
  rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
  exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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 suffices₁ 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)
have 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)
Tactic: classical
  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
  ext i
  apply b.repr.injective
  letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
  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 : 𝕜)
  rw [mul_one] at this
  rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
  exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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 suffices₁ 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)
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)
⊢ 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)
have h₁ : ∀ (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: classical
  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
  ext i
  apply b.repr.injective
  letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
  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 : 𝕜)
  rw [mul_one] at this
  rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
  exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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
have 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)
Tactic: refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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 ι
⊢ ∑ 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)
have 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))
Tactic: simp only [SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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))
have 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))
Tactic: refine sum_mem ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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))
have 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)
Tactic: refine smul_mem _ _ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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₂ :
  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))))
    ⊤
have rw₃ : ∀ ⦃x : E⦄,
  Membership.mem (γ := Submodule 𝕜 E)
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
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₂ :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
rw₃ :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Submodule 𝕜 E)
      (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw₄ : ∀ ⦃x : E⦄ (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)
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩