𝕜 : Type u_1
E : Type u_2
F : Type ?u.3108160
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : inner x y = 0
⊢ 2 = 0 ∨ ↑re (inner x y) = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3108160
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : inner x y = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
rw [@norm_add_mul_self 𝕜, add_right_cancel_iff, add_right_eq_self, mul_eq_zero]
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3108160
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : inner x y = 0
⊢ ↑re (inner x y) = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3108160
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : inner x y = 0
⊢ 2 = 0 ∨ ↑re (inner x y) = 0
apply Or.inr
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3108160
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : inner x y = 0
⊢ ↑re (inner x y) = 0
simp only [h, zero_re']