V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ sin (arccos (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = sqrt (inner x x * inner y y - inner x y * inner x y)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ sin (angle x y) * (‖x‖ * ‖y‖) = sqrt (inner x x * inner y y - inner x y * inner x y)
unfold angle
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ sin (arccos (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = sqrt (inner x x * inner y y - inner x y * inner x y)
rw [Real.sin_arccos, ← Real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
  ← Real.sqrt_mul' _ (mul_self_nonneg _), sq,
  Real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
  real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
by_cases h : ‖x‖ * ‖y‖ = 0
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
rw [show ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) by ring, h, MulZeroClass.mul_zero,
  MulZeroClass.mul_zero, zero_sub]
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hx : ‖x‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))

case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hy : ‖y‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
cases' eq_zero_or_eq_zero_of_mul_eq_zero h with hx hy
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
ring
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hx : x = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hx : ‖x‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
rw [norm_eq_zero] at hx
no goals
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hx : x = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
rw [hx, inner_zero_left, MulZeroClass.zero_mul, neg_zero]
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hy : y = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hy : ‖y‖ = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
rw [norm_eq_zero] at hy
no goals
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ‖x‖ * ‖y‖ = 0
hy : y = 0
⊢ sqrt 0 = sqrt (-(inner x y * inner x y))
rw [hy, inner_zero_right, MulZeroClass.zero_mul, neg_zero]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ sqrt (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) - inner x y * inner x y) = sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ sqrt ((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
field_simp [h]
no goals
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ sqrt (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) - inner x y * inner x y) = sqrt (‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)
ring_nf