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