no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3233193
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ inner x y = 1 ↔ x = y
convert inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2 <;> simp [hx, hy]