𝕜 : Type u_1
E : Type u_2
F : Type ?u.2621009
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑im (inner x y) =
    (‖x‖ * ‖x‖ - 2 * -↑im (inner x y) + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -↑im (inner x y) + ‖I • y‖ * ‖I • y‖)) / 4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2621009
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑im (inner x y) = (‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4
simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2621009
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑im (inner x y) =
    (‖x‖ * ‖x‖ - 2 * -↑im (inner x y) + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -↑im (inner x y) + ‖I • y‖ * ‖I • y‖)) / 4
ring