-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
neg :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁) • (r₁ • x + r₂ • y) + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₁ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁) • r₁ • x + (-r₃ / r₁) • r₂ • y + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₂ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₁) • x + (-r₃ / r₁) • r₂ • y + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₃ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₁) • x + (-r₃ / r₁ * r₂) • y + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₄ :
  (o.oangle (r₁ • x + r₂ • y) (-r₃ • x + (-r₃ / r₁ * r₂) • y + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₅ :
  (o.oangle (r₁ • x + r₂ • y) (-(r₃ • x) + (-r₃ / r₁ * r₂) • y + (r₃ • x + r₄ • y))).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₆ :
  (o.oangle (r₁ • x + r₂ • y) (-(r₃ • x) + (-r₃ / r₁ * r₂) • y + r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₇ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₂) • y + -(r₃ • x) + r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₈ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₂) • y - r₃ • x + r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₉ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₂) • y + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₁₀ :
  (o.oangle (r₁ • x + r₂ • y) ((-r₃ / r₁ * r₂ + r₄) • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₁₁ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-r₃ / r₁ * r₂ + r₄) : SignType)
      (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
neg₁₂ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-r₃ / r₁ * r₂ + r₄) : SignType)
      (HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign) =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
have neg₁₃ : HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : ℝ) → SignType) (-r₃ / r₁ * r₂ + r₄) : SignType)
      ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) *
    (o.oangle x y).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
Tactic: rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add,
      smul_smul, smul_smul, div_mul_cancel₀ _ hr₁, neg_smul, ← add_assoc, add_comm (-(r₃ • x)), ←
      sub_eq_add_neg, sub_add_cancel, ← add_smul, oangle_sign_smul_right,
      oangle_sign_smul_add_smul_left, ← mul_assoc, ← sign_mul, add_mul, mul_assoc, mul_comm r₂ r₁, ←
      mul_assoc, div_mul_cancel₀ _ hr₁, add_comm, neg_mul, ← sub_eq_add_neg, mul_comm r₄,
      mul_comm r₃]