case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.851438
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
⊢ (fun i =>
      inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
        inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y) =
    fun b_1 =>
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) b_1 • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) b_1)
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.851438
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
⊢ HasSum
    (fun i =>
      inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
        inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y)
    (inner x y)
convert (b.hasSum_repr y).mapL (innerSL _ x) using 1
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.851438
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
      inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y =
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.851438
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
⊢ (fun i =>
      inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
        inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y) =
    fun b_1 =>
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) b_1 • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) b_1)
ext i
no goals
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.851438
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
      inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y =
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]