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
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
⊢ (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₃ • 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
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
⊢ (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₃ • 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
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
⊢ (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₃ • 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
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
⊢ (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₂) • 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
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
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
⊢ (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₂) • 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
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
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
⊢ (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₂) • y + 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
h : ‖x‖ = ‖y‖
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have pos : ∀ (hn : x = y), |(o.oangle (y - x) y).toReal| < π / 2
Tactic: by_cases hn : x = y
-- 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
h : ‖x‖ = ‖y‖
pos : ∀ (hn : x = y), |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have neg : ∀ (hn : ¬x = y), |(o.oangle (y - x) y).toReal| < π / 2
Tactic: by_cases hn : x = y
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
| (o.oangle (y - x) y).sign
have rw : (o.oangle y x).sign
Tactic: rw [oangle_sign_sub_left_swap]
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign
have conv_rhs : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle y x).sign
Tactic: conv_rhs => rw [oangle_sign_sub_left_swap]
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle y x).sign
have rw : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign =
  ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign
Tactic: rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
rw :
  (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign =
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle y x).sign
have rw₁ : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign
Tactic: rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hs : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign
Tactic: have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := by
    conv_rhs => rw [oangle_sign_sub_left_swap]
    rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hs₁ : o.oangle (y - x) y = (↑π : Real.Angle) ∨ |(o.oangle (y - x) y).toReal| < π / 2
Tactic: rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs
Cleared hypotheses: hs
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle (y - x) y = (↑π : Real.Angle) ∨ |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have neg : ∀ (hs : o.oangle (y - x) y = (↑π : Real.Angle)), |(o.oangle (y - x) y).toReal| < π / 2
Tactic: rcases hs with (hs | hs)
Cleared hypotheses: hs
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle (y - x) y = (↑π : Real.Angle) ∨ |(o.oangle (y - x) y).toReal| < π / 2
neg : ∀ (hs : o.oangle (y - x) y = (↑π : Real.Angle)), |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have neg₁ : ∀ (hs : |(o.oangle (y - x) y).toReal| < π / 2), |(o.oangle (y - x) y).toReal| < π / 2
Tactic: rcases hs with (hs | hs)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle (y - x) y = (↑π : Real.Angle)
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hs₁ : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)
Tactic: rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, neg_sub] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hy : y ≠ 0
Tactic: rcases hs with ⟨hy, -, hr⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)
hy : y ≠ 0
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr : SameRay ℝ y (x - y)
Tactic: rcases hs with ⟨hy, -, hr⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
hr : SameRay ℝ y (x - y)
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr₁ : ∃ (r : ℝ), 0 ≤ r ∧ r • y = x - y
Tactic: rw [← exists_nonneg_left_iff_sameRay hy] at hr
Cleared hypotheses: hr
-- 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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
hr : ∃ (r : ℝ), 0 ≤ r ∧ r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have neg : ∀ (r : ℝ) (hr0 : 0 ≤ r) (hr : r • y = x - y), |(o.oangle (y - x) y).toReal| < π / 2
Tactic: rcases hr with ⟨r, hr0, hr⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr₁ : r • y + y = x
Tactic: rw [eq_sub_iff_add_eq] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y + y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr₁ : r • y + HSMul.hSMul (α := ℝ) 1 y = x
Tactic: nth_rw 2 [← one_smul ℝ y] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y + HSMul.hSMul (α := ℝ) 1 y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr₁ : (r + 1) • y = x
Tactic: rw [← add_smul] at hr
Cleared hypotheses: hr