awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
hx : (x, y) ∈ s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have hy : (x, r • x + y) ∈ s
Tactic: have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _)
-- 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 : ℝ
⊢ (o.oangle (x + r • y) y).sign = (o.oangle x y).sign
have simp_rw : (-o.oangle y (x + r • y)).sign = (-o.oangle y x).sign
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]
-- 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 : ℝ
simp_rw : (-o.oangle y (x + r • y)).sign = (-o.oangle y x).sign
⊢ (o.oangle (x + r • y) y).sign = (o.oangle x y).sign
have simp_rw₁ : -(o.oangle y (x + r • y)).sign = -(o.oangle y x).sign
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]
-- 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 : ℝ
simp_rw : (-o.oangle y (x + r • y)).sign = (-o.oangle y x).sign
simp_rw₁ : -(o.oangle y (x + r • y)).sign = -(o.oangle y x).sign
⊢ (o.oangle (x + r • y) y).sign = (o.oangle x y).sign
have simp_rw₂ : -(o.oangle y (r • y + x)).sign = -(o.oangle y x).sign
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]
-- 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 : ℝ
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign
have rw : (o.oangle x (y + -(r • x))).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]
-- 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 : ℝ
rw : (o.oangle x (y + -(r • x))).sign = (o.oangle x y).sign
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign
have rw₁ : (o.oangle x (y + -r • x)).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]
-- 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 : ℝ
rw : (o.oangle x (y + -(r • x))).sign = (o.oangle x y).sign
rw₁ : (o.oangle x (y + -r • x)).sign = (o.oangle x y).sign
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign
have rw₂ : (o.oangle x (-r • x + y)).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]
-- 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 : ℝ
rw : (o.oangle x (y + -(r • x))).sign = (o.oangle x y).sign
rw₁ : (o.oangle x (y + -r • x)).sign = (o.oangle x y).sign
rw₂ : (o.oangle x (-r • x + y)).sign = (o.oangle x y).sign
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign
have rw₃ : (o.oangle x y).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]
-- 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 : ℝ
⊢ (o.oangle (x - r • y) y).sign = (o.oangle x y).sign
have rw : (o.oangle (x + -(r • y)) y).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]
-- 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 : ℝ
rw : (o.oangle (x + -(r • y)) y).sign = (o.oangle x y).sign
⊢ (o.oangle (x - r • y) y).sign = (o.oangle x y).sign
have rw₁ : (o.oangle (x + -r • y) y).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]
-- 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 : ℝ
rw : (o.oangle (x + -(r • y)) y).sign = (o.oangle x y).sign
rw₁ : (o.oangle (x + -r • y) y).sign = (o.oangle x y).sign
⊢ (o.oangle (x - r • y) y).sign = (o.oangle x y).sign
have rw₂ : (o.oangle x y).sign = (o.oangle x y).sign
Tactic: rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]
-- 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
⊢ (o.oangle x (x + y)).sign = (o.oangle x y).sign
have rw : (o.oangle x (x + y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x + y)).sign
Tactic: rw [← o.oangle_sign_smul_add_right x y 1, one_smul]
-- 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
rw : (o.oangle x (x + y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x + y)).sign
⊢ (o.oangle x (x + y)).sign = (o.oangle x y).sign
have rw₁ : (o.oangle x (x + y)).sign = (o.oangle x (x + y)).sign
Tactic: rw [← o.oangle_sign_smul_add_right x y 1, one_smul]
-- 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
⊢ (o.oangle (x + y) y).sign = (o.oangle x y).sign
have rw : (o.oangle (x + y) y).sign = (o.oangle (x + HSMul.hSMul (α := ℝ) 1 y) y).sign
Tactic: rw [← o.oangle_sign_add_smul_left x y 1, one_smul]
-- 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
rw : (o.oangle (x + y) y).sign = (o.oangle (x + HSMul.hSMul (α := ℝ) 1 y) y).sign
⊢ (o.oangle (x + y) y).sign = (o.oangle x y).sign
have rw₁ : (o.oangle (x + y) y).sign = (o.oangle (x + y) y).sign
Tactic: rw [← o.oangle_sign_add_smul_left x y 1, one_smul]
-- 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
⊢ (o.oangle x (y - x)).sign = (o.oangle x y).sign
have rw : (o.oangle x (y - x)).sign = (o.oangle x (y - HSMul.hSMul (α := ℝ) 1 x)).sign
Tactic: rw [← o.oangle_sign_sub_smul_right x y 1, one_smul]
-- 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
rw : (o.oangle x (y - x)).sign = (o.oangle x (y - HSMul.hSMul (α := ℝ) 1 x)).sign
⊢ (o.oangle x (y - x)).sign = (o.oangle x y).sign
have rw₁ : (o.oangle x (y - x)).sign = (o.oangle x (y - x)).sign
Tactic: rw [← o.oangle_sign_sub_smul_right x y 1, one_smul]
-- 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
⊢ (o.oangle (x - y) y).sign = (o.oangle x y).sign
have rw : (o.oangle (x - y) y).sign = (o.oangle (x - HSMul.hSMul (α := ℝ) 1 y) y).sign
Tactic: rw [← o.oangle_sign_sub_smul_left x y 1, one_smul]
-- 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
rw : (o.oangle (x - y) y).sign = (o.oangle (x - HSMul.hSMul (α := ℝ) 1 y) y).sign
⊢ (o.oangle (x - y) y).sign = (o.oangle x y).sign
have rw₁ : (o.oangle (x - y) y).sign = (o.oangle (x - y) y).sign
Tactic: rw [← o.oangle_sign_sub_smul_left x y 1, one_smul]
-- 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 : ℝ
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
have rw : (o.oangle x (r • x - y)).sign = (o.oangle x (-y)).sign
Tactic: rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]
-- 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 : ℝ
rw : (o.oangle x (r • x - y)).sign = (o.oangle x (-y)).sign
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
have rw₁ : (o.oangle x (r • x + -y)).sign = (o.oangle x (-y)).sign
Tactic: rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]
-- 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 : ℝ
rw : (o.oangle x (r • x - y)).sign = (o.oangle x (-y)).sign
rw₁ : (o.oangle x (r • x + -y)).sign = (o.oangle x (-y)).sign
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
have rw₂ : (o.oangle x (-y)).sign = (o.oangle x (-y)).sign
Tactic: rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]
-- 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 : ℝ
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
have rw : (o.oangle (r • y - x) y).sign = (o.oangle (-x) y).sign
Tactic: rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]
-- 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 : ℝ
rw : (o.oangle (r • y - x) y).sign = (o.oangle (-x) y).sign
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
have rw₁ : (o.oangle (-x + r • y) y).sign = (o.oangle (-x) y).sign
Tactic: rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]
-- 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 : ℝ
rw : (o.oangle (r • y - x) y).sign = (o.oangle (-x) y).sign
rw₁ : (o.oangle (-x + r • y) y).sign = (o.oangle (-x) y).sign
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
have rw₂ : (o.oangle (-x) y).sign = (o.oangle (-x) y).sign
Tactic: rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]
-- 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
⊢ (o.oangle x (x - y)).sign = -(o.oangle x y).sign
have rw : (o.oangle x (x - y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x - y)).sign
Tactic: rw [← o.oangle_sign_smul_sub_right x y 1, one_smul]
-- 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
rw : (o.oangle x (x - y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x - y)).sign
⊢ (o.oangle x (x - y)).sign = -(o.oangle x y).sign
have rw₁ : (o.oangle x (x - y)).sign = (o.oangle x (x - y)).sign
Tactic: rw [← o.oangle_sign_smul_sub_right x y 1, one_smul]
-- 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
⊢ (o.oangle (y - x) y).sign = -(o.oangle x y).sign
have rw : (o.oangle (y - x) y).sign = (o.oangle (HSMul.hSMul (α := ℝ) 1 y - x) y).sign
Tactic: rw [← o.oangle_sign_smul_sub_left x y 1, one_smul]
-- 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
rw : (o.oangle (y - x) y).sign = (o.oangle (HSMul.hSMul (α := ℝ) 1 y - x) y).sign
⊢ (o.oangle (y - x) y).sign = -(o.oangle x y).sign
have rw₁ : (o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign
Tactic: rw [← o.oangle_sign_smul_sub_left x y 1, one_smul]
-- 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
⊢ (o.oangle y (y - x)).sign = (o.oangle x y).sign
have rw : -(o.oangle y x).sign = (o.oangle x y).sign
Tactic: rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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
rw : -(o.oangle y x).sign = (o.oangle x y).sign
⊢ (o.oangle y (y - x)).sign = (o.oangle x y).sign
have rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
Tactic: rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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
rw : -(o.oangle y x).sign = (o.oangle x y).sign
rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
⊢ (o.oangle y (y - x)).sign = (o.oangle x y).sign
have rw₂ : -(o.oangle y x).sign = -(o.oangle y x).sign
Tactic: rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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
⊢ (o.oangle (x - y) x).sign = (o.oangle x y).sign
have rw : -(o.oangle y x).sign = (o.oangle x y).sign
Tactic: rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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
rw : -(o.oangle y x).sign = (o.oangle x y).sign
⊢ (o.oangle (x - y) x).sign = (o.oangle x y).sign
have rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
Tactic: rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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
rw : -(o.oangle y x).sign = (o.oangle x y).sign
rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
⊢ (o.oangle (x - y) x).sign = (o.oangle x y).sign
have rw₂ : -(o.oangle y x).sign = -(o.oangle y x).sign
Tactic: rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]
-- 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₂ : ℝ
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign
have simp_rw : (-o.oangle y (r₁ • x + r₂ • y)).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-o.oangle y x).sign
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
    mul_neg]
-- 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₂ : ℝ
simp_rw :
  (-o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-o.oangle y x).sign
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign
have simp_rw₁ : -(o.oangle y (r₁ • x + r₂ • y)).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
    mul_neg]
-- 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₂ : ℝ
simp_rw :
  (-o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-o.oangle y x).sign
simp_rw₁ :
  -(o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign
have simp_rw₂ : -(o.oangle y (r₂ • y + r₁ • x)).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
    mul_neg]
-- 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₂ : ℝ
simp_rw :
  (-o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-o.oangle y x).sign
simp_rw₁ :
  -(o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
simp_rw₂ :
  -(o.oangle y (r₂ • y + r₁ • x)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign
have simp_rw₃ : -HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle y x).sign =
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
Tactic: simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
    mul_neg]
-- 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₄ : ℝ
⊢ (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 : ∀ (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
Tactic: by_cases hr₁ : r₁ = 0
-- 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₄ : ℝ
pos :
  ∀ (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
⊢ (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 : ∀ (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
Tactic: by_cases hr₁ : r₁ = 0
-- 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 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
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
⊢ (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₂ * 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]