no goals
𝕜 : Type ?u.4079769
E : Type ?u.4079772
F : Type ?u.4079775
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
⊢ inner x y = (↑(starRingEnd ℂ) (↑f x) * ↑f y).re
rw [← Complex.inner, f.inner_map_map]