-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem hasSum_repr_symm (b : HilbertBasis ι 𝕜 E) (f : ℓ²(ι, 𝕜)) :
    HasSum (fun i => f i • b i) (b.repr.symm f)

Proof state:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ lp.single 2 i (↑f i) = b.repr (b.repr.symm ((fun i => lp.single 2 i (↑f i)) i))

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

Result:
no goals

Proof state:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Tactic:
letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance

Result:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
H : (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
⊢ HasSum (fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)) (b.repr.symm f)

Tactic:
have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
H : (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
this : HasSum (fun i => lp.single 2 i (↑f i)) f
⊢ HasSum (fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)) (b.repr.symm f)

Proof state:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

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 : 𝕜)

Result:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i * 1) = ↑f i • lp.single 2 i 1
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
H : (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
⊢ HasSum (fun i => ↑f i • b i) (b.repr.symm f)

Tactic:
rw [H]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
H : (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
⊢ HasSum (fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)) (b.repr.symm f)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
⊢ HasSum (fun i => ↑f i • b i) (b.repr.symm f)

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 [LinearIsometryEquiv.map_smul, b.repr_self, ← this,
  LinearIsometryEquiv.coe_toContinuousLinearEquiv]
exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
H : (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
this : HasSum (fun i => lp.single 2 i (↑f i)) f
⊢ HasSum (fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)) (b.repr.symm f)

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

Result:
no goals

Proof state:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

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

Result:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ lp.single 2 i (↑f i) = b.repr (b.repr.symm ((fun i => lp.single 2 i (↑f i)) i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
⊢ HasSum (fun i => ↑f i • b i) (b.repr.symm f)

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

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
⊢ (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)