-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem sin_angle_mul_norm_mul_norm (x y : V) :
    Real.sin (angle x y) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (arccos (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = √(inner x x * inner y y - inner x y * inner x y)

Tactic:
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]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Proof state:
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hy : y = 0
⊢ √0 = √(-(inner x y * inner x y))

Tactic:
rw [hy, inner_zero_right, zero_mul, neg_zero]

Result:
no goals

Proof state:
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hx : ‖x‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

Tactic:
rw [norm_eq_zero] at hx

Result:
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hx : x = 0
⊢ √0 = √(-(inner x y * inner x y))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) * (‖x‖ * ‖y‖) = √(inner x x * inner y y - inner x y * inner x y)

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (arccos (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = √(inner x x * inner y y - inner x y * inner x y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
ring

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Tactic:
field_simp [h]

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ √(‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) - inner x y * inner x y) = √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

Tactic:
rcases eq_zero_or_eq_zero_of_mul_eq_zero h with hx | hy

Result:
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hx : ‖x‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hy : ‖y‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

Proof state:
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hy : ‖y‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

Tactic:
rw [norm_eq_zero] at hy

Result:
case pos.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hy : y = 0
⊢ √0 = √(-(inner x y * inner x y))

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Tactic:
rw [show ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) by ring, h, mul_zero,
  mul_zero, zero_sub]

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ √0 = √(-(inner x y * inner x y))

Proof state:
case pos.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
hx : x = 0
⊢ √0 = √(-(inner x y * inner x y))

Tactic:
rw [hx, inner_zero_left, zero_mul, neg_zero]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Tactic:
by_cases h : ‖x‖ * ‖y‖ = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ * ‖y‖ = 0
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ √((1 - inner x y / (‖x‖ * ‖y‖) * (inner x y / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ¬‖x‖ * ‖y‖ = 0
⊢ √(‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) - inner x y * inner x y) = √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - inner x y * inner x y)

Tactic:
ring_nf

Result:
no goals