no goals
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ‖↑(extendTo𝕜' fr) x‖ ^ 2 = ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x)
rw [IsROrC.conj_mul, normSq_eq_def', ofReal_re]
no goals
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x) =
    ↑fr (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) • x)
rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]