-- 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)
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))
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))
h₃ :
  ∀ (i : ι)
    (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))
h₄ :
  ∀ (i : ι)
    (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))
⊢ 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 : ι)
  (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: 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