𝕜 : Type u_4
E : Type u_2
F : Type ?u.3676885
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
l : (i : ι) → G i
s : Finset ι
this : ↑‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ↑‖l i‖ ^ 2
⊢ ‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ‖l i‖ ^ 2
𝕜 : Type u_4
E : Type u_2
F : Type ?u.3676885
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
l : (i : ι) → G i
s : Finset ι
⊢ ‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ‖l i‖ ^ 2
have : ((‖∑ i in s, V i (l i)‖ : ℝ) : 𝕜) ^ 2 = ∑ i in s, ((‖l i‖ : ℝ) : 𝕜) ^ 2 := by
  simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]
no goals
𝕜 : Type u_4
E : Type u_2
F : Type ?u.3676885
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
l : (i : ι) → G i
s : Finset ι
this : ↑‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ↑‖l i‖ ^ 2
⊢ ‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ‖l i‖ ^ 2
exact_mod_cast this
no goals
𝕜 : Type u_4
E : Type u_2
F : Type ?u.3676885
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
l : (i : ι) → G i
s : Finset ι
⊢ ↑‖∑ i in s, ↑(V i) (l i)‖ ^ 2 = ∑ i in s, ↑‖l i‖ ^ 2
simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]