no goals
ι : Type u_1
ι' : Type ?u.652079
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.652088
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.652108
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.652126
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.652146
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ inner v (single i a) = a * ↑(starRingEnd ((fun x => 𝕜) i)) (v i)
simp [apply_ite conj, mul_comm]