awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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₂ : (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
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]
-- 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
⊢ (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₃ : (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
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]
-- 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
⊢ (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₄ : (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-(r₂ * 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]
-- 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
⊢ (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₅ : (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign =
  HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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) (o.oangle y (r₃ • x + r₄ • y)).sign =
  HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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) (o.oangle y (r₄ • y + r₃ • x)).sign =
  HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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 y x).sign) =
  HMul.hMul (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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.sign : (a : ℝ) → SignType) (r₂ * 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]
-- 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
⊢ (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 : (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
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₃]
-- 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
⊢ (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₁ : (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
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₃]
-- 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
⊢ (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₂ : (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
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₃]
-- 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
⊢ (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₃ : (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
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₃]