case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬(x = 0 ∧ y = 0)
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
by_cases h0 : x = 0 ∧ y = 0
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬(x = 0 ∧ y = 0)
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
rw [not_and_or] at h0
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x + y‖ ≠ 0
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x + y‖ ≠ 0
rw [← mul_self_ne_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real h]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
refine' (ne_of_lt _).symm
case neg.h.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
rcases h0 with (h0 | h0)
no goals
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
simp [h0]
no goals
case neg.h.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
no goals
case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))