case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
y : E
⊢ inner 0 y = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y

case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
rcases eq_or_ne x 0 with (rfl | h₀)
no goals
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
y : E
⊢ inner 0 y = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y
simp
case inr.ha
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
⊢ ↑‖x‖ ≠ 0
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
rw [inner_eq_norm_mul_iff_div h₀, div_eq_inv_mul, mul_smul, inv_smul_eq_iff₀]
no goals
case inr.ha
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3212961
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
⊢ ↑‖x‖ ≠ 0
rwa [Ne.def, ofReal_eq_zero, norm_eq_zero]