-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.cos (angle x (x - y) + angle y (y - x)) = -Real.cos (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)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖))
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖

Tactic:
have H2 :
  ⟪x, x⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, x⟫ - ⟪x, y⟫) * (⟪x, x⟫ - ⟪x, y⟫) =
    ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫ := by
  ring

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)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖))
H2 :
  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
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖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
hyn : ‖y‖ ≠ 0
hxyn : ‖x - y‖ ≠ 0
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖

Tactic:
have H1 :
  Real.sin (angle x (x - y)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) *
      (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖)) := by
  ring

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)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖))
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖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
hyn : ‖y‖ ≠ 0
hxyn : ‖x - y‖ ≠ 0
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
          Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
        ‖x‖ *
      ‖y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖

Tactic:
apply mul_right_cancel₀ hxyn

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
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
            Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
          ‖x‖ *
        ‖y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.cos (angle x (x - y) + angle y (y - x)) = -Real.cos (angle x y)

Tactic:
by_cases hxy : x = y

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x = y
⊢ Real.cos (angle x (x - y) + angle y (y - x)) = -Real.cos (angle x y)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : ¬x = y
⊢ Real.cos (angle x (x - y) + angle y (y - x)) = -Real.cos (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)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖))
H2 :
  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
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖

Tactic:
have H3 :
  ⟪y, y⟫ * (⟪y, y⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪x, x⟫)) - (⟪y, y⟫ - ⟪x, y⟫) * (⟪y, y⟫ - ⟪x, y⟫) =
    ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫ := by
  ring

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)) * Real.sin (angle y (y - x)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖ =
    Real.sin (angle x (x - y)) * (‖x‖ * ‖x - y‖) * (Real.sin (angle y (y - x)) * (‖y‖ * ‖x - y‖))
H2 :
  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
H3 :
  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
⊢ (inner x (x - y) / (‖x‖ * ‖x - y‖) * (inner y (y - x) / (‖y‖ * ‖y - x‖)) -
              Real.sin (angle x (x - y)) * Real.sin (angle y (y - x))) *
            ‖x‖ *
          ‖y‖ *
        ‖x - y‖ *
      ‖x - y‖ =
    -(inner x y / (‖x‖ * ‖y‖)) * ‖x‖ * ‖y‖ * ‖x - y‖ * ‖x - y‖