-- 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
pos :
  (o.oangle (HSMul.hSMul (α := ℝ) 0 x + r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (0 * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
pos₁ :
  (o.oangle (0 + r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (0 * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign
pos₂ :
  (o.oangle (0 + r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (0 - r₂ * r₃) : SignType) (o.oangle x y).sign
pos₃ :
  (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (0 - r₂ * r₃) : SignType) (o.oangle x y).sign
pos₄ :
  (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-(r₂ * r₃)) : SignType) (o.oangle x y).sign
pos₅ :
  (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * r₃) : SignType) (o.oangle x y).sign
pos₆ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType) (o.oangle y (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * r₃) : SignType) (o.oangle x y).sign
pos₇ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType) (o.oangle y (r₄ • y + r₃ • x)).sign =
    HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * r₃) : SignType) (o.oangle x y).sign
pos₈ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType)
      (HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₃ : SignType) (o.oangle y x).sign) =
    HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * r₃) : SignType) (o.oangle x y).sign
pos₉ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 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₃) : SignType) (o.oangle x y).sign
pos₁₀ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 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₃) : SignType) (o.oangle x y).sign
pos₁₁ :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType)
      (HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₃ : SignType) (-(o.oangle x y).sign)) =
    -HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType)
          ((SignType.sign : (a : ℝ) → SignType) 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 pos₁₂ : HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType)
    (-HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₃ : SignType) (o.oangle x y).sign) =
  -HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType)
        ((SignType.sign : (a : ℝ) → SignType) r₃ : SignType) *
    (o.oangle x y).sign
Tactic: rw [hr₁, zero_smul, zero_mul, zero_add, zero_sub, Left.sign_neg,
      oangle_sign_smul_left, add_comm, oangle_sign_smul_add_smul_right, oangle_rev,
      Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc]