V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x + y)
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos,
  norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
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
hx : x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

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
hx : ¬x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
by_cases hx : x = 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
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖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
hx : ¬x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
rw [div_lt_one (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2
  (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))), Real.lt_sqrt (norm_nonneg _), pow_two]
no goals
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
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
simpa [hx] using 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
hx : x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
simp [hx]