-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem sin_angle_sub_add_angle_sub_rev_eq_sin_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.sin (angle x (x - y) + angle y (y - x)) = Real.sin (angle x y)

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : ¬x = y
hxn : ‖x‖ ≠ 0
hyn : ‖y‖ ≠ 0
hxyn : ‖x - y‖ ≠ 0
H1 :
  Real.sin (angle x (x - y)) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) * ‖y‖
H2 :
  inner x (x - y) / (‖x‖ * ‖y - x‖) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖y - x‖ =
    inner x (x - y) / (‖x‖ * ‖y - x‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖y - x‖)) * ‖x‖
H3 :
  inner x x * (inner x x - inner x y - (inner x y - inner y y)) - (inner x x - inner x y) * (inner x x - inner x y) =
    inner x x * inner y y - inner x y * inner x y
H4 :
  inner y y * (inner y y - inner x y - (inner x y - inner x x)) - (inner y y - inner x y) * (inner y y - inner x y) =
    inner x x * inner y y - inner x y * inner x y
⊢ (Real.sin (angle x (x - y)) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) +
              inner x (x - y) / (‖x‖ * ‖x - y‖) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    Real.sin (angle x y) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖

Tactic:
rw [right_distrib, right_distrib, right_distrib, right_distrib, H1, sin_angle_mul_norm_mul_norm,
  norm_sub_rev x y, H2, sin_angle_mul_norm_mul_norm, norm_sub_rev y x,
  mul_assoc (Real.sin (angle x y)), sin_angle_mul_norm_mul_norm, inner_sub_left, inner_sub_left,
  inner_sub_right, inner_sub_right, inner_sub_right, inner_sub_right, real_inner_comm x y, H3,
  H4, real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm,
  real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two]

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : ¬x = y
hxn : ‖x‖ ≠ 0
hyn : ‖y‖ ≠ 0
hxyn : ‖x - y‖ ≠ 0
H1 :
  Real.sin (angle x (x - y)) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) * ‖y‖
H2 :
  inner x (x - y) / (‖x‖ * ‖y - x‖) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖y - x‖ =
    inner x (x - y) / (‖x‖ * ‖y - x‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖y - x‖)) * ‖x‖
H3 :
  inner x x * (inner x x - inner x y - (inner x y - inner y y)) - (inner x x - inner x y) * (inner x x - inner x y) =
    inner x x * inner y y - inner x y * inner x y
H4 :
  inner y y * (inner y y - inner x y - (inner x y - inner x x)) - (inner y y - inner x y) * (inner y y - inner x y) =
    inner x x * inner y y - inner x y * inner x y
⊢ √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) -
                (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 * ((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2)) *
            ((‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2) / (‖y‖ * ‖x - y‖)) *
          ‖y‖ *
        ‖x - y‖ +
      (‖x‖ * ‖x‖ - (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2) / (‖x‖ * ‖x - y‖) *
            √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) -
                (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 * ((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2)) *
          ‖x‖ *
        ‖x - y‖ =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) -
            (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 * ((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2)) *
        ‖x - y‖ *
      ‖x - y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : ¬x = y
hxn : ‖x‖ ≠ 0
⊢ Real.sin (angle x (x - y)) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) +
      inner x (x - y) / (‖x‖ * ‖x - y‖) * Real.sin (angle y (y - x)) =
    Real.sin (angle x y)

Tactic:
have hyn : ‖y‖ ≠ 0 := fun h => hy (norm_eq_zero.1 h)

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : ¬x = y
hxn : ‖x‖ ≠ 0
hyn : ‖y‖ ≠ 0
⊢ Real.sin (angle x (x - y)) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) +
      inner x (x - y) / (‖x‖ * ‖x - y‖) * Real.sin (angle y (y - x)) =
    Real.sin (angle x y)