awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : 0 < r
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

Tactic:
simp [hlt]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
hp₃ : p₃ ≠ p
⊢ ∡ p₁ p p₂ + ∡ p₂ p p₃ = ∡ p₁ p p₃

Tactic:
o.oangle_add (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)

Premises used: EuclideanGeometry.oangle, Orientation.oangle_add, Iff.mpr, vsub_ne_zero, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
hp₃ : p₃ ≠ p
⊢ ∡ p₂ p p₃ + ∡ p₁ p p₂ = ∡ p₁ p p₃

Tactic:
o.oangle_add_swap (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)

Premises used: EuclideanGeometry.oangle, Iff.mpr, Orientation.oangle_add_swap, vsub_ne_zero, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
hp₃ : p₃ ≠ p
⊢ ∡ p₁ p p₃ - ∡ p₁ p p₂ = ∡ p₂ p p₃

Tactic:
o.oangle_sub_left (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.oangle_sub_left, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
hp₃ : p₃ ≠ p
⊢ ∡ p₁ p p₃ - ∡ p₂ p p₃ = ∡ p₁ p p₂

Tactic:
o.oangle_sub_right (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, EuclideanGeometry.o, Orientation.oangle_sub_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
hp₃ : p₃ ≠ p
⊢ ∡ p₁ p p₂ + ∡ p₂ p p₃ + ∡ p₃ p p₁ = 0

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
simp_rw [dist_eq_norm_vsub V] at h

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
rw₁ : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
rw₂ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
rw₃ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
rw₄ rw₅ :
  Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃) = Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Tactic:
rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

Premises used: EuclideanGeometry.oangle, Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq, vsub_sub_vsub_cancel_left, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : dist p₁ p₂ = dist p₁ p₃
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
simp_rw [dist_eq_norm_vsub V] at h

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))

Tactic:
o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h

Premises used: Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
h₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))
convert! : p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))

Tactic:
convert! o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1

Premises used: Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
h₂ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (-(p₁ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
h₃ h₄ : Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)

Tactic:
rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]

Premises used: neg_vsub_eq_vsub_rev, EuclideanGeometry.o, Orientation.oangle_neg_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)))
⊢ (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))

Tactic:
rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

Premises used: Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃

Tactic:
simpa using hn
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : |(Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]

Premises used: EuclideanGeometry.oangle, vsub_sub_vsub_cancel_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2

Tactic:
o.abs_oangle_sub_right_toReal_lt_pi_div_two h

Premises used: EuclideanGeometry.o, Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2

Tactic:
exact o.abs_oangle_sub_right_toReal_lt_pi_div_two h

Premises used: EuclideanGeometry.o, Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
oangle_eq_oangle_of_dist_eq h ▸ abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq h

Premises used: EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, Eq.rec, EuclideanGeometry.oangle_eq_oangle_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
⊢ (∡ p₁ p p₂).cos = Real.cos (∠ p₁ p p₂)

Tactic:
o.cos_oangle_eq_cos_angle (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.cos_oangle_eq_cos_angle, EuclideanGeometry.o, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
⊢ ∡ p₁ p p₂ = (↑(∠ p₁ p p₂) : Real.Angle) ∨ ∡ p₁ p p₂ = -(↑(∠ p₁ p p₂) : Real.Angle)

Tactic:
o.oangle_eq_angle_or_eq_neg_angle (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.oangle_eq_angle_or_eq_neg_angle, EuclideanGeometry.o, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
hp₁ : p₁ ≠ p
hp₂ : p₂ ≠ p
⊢ ∠ p₁ p p₂ = |(∡ p₁ p p₂).toReal|

Tactic:
o.angle_eq_abs_oangle_toReal (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.angle_eq_abs_oangle_toReal, EuclideanGeometry.o, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₁ -ᵥ p = 0 ∨
    p₂ -ᵥ p = 0 ∨
      InnerProductGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) = 0 ∨ InnerProductGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) = π

Tactic:
o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h

Premises used: EuclideanGeometry.o, Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
h₁ : p₁ = p ↔ p₁ -ᵥ p = 0
h₂ : p₂ = p ↔ p₂ -ᵥ p = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π

Tactic:
convert! o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h

Premises used: EuclideanGeometry.o, Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₁ = p ↔ p₁ -ᵥ p = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₂ = p ↔ p₂ -ᵥ p = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆

Tactic:
o.oangle_eq_of_angle_eq_of_sign_eq h hs

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_of_angle_eq_of_sign_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
hp₁ : p₁ ≠ p₂
hp₃ : p₃ ≠ p₂
hp₄ : p₄ ≠ p₅
hp₆ : p₆ ≠ p₅
hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign
⊢ ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆ ↔ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆

Tactic:
o.angle_eq_iff_oangle_eq_of_sign_eq (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₃) (vsub_ne_zero.2 hp₄)
    (vsub_ne_zero.2 hp₆) hs

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.angle_eq_iff_oangle_eq_of_sign_eq, EuclideanGeometry.o, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
⊢ ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)

Tactic:
have h_1 := EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle h1.symm h2.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
⊢ ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)

Tactic:
have h_2 := EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle h3.symm h4.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : ∀ (h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
inr : ∀ (h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
rcases h_1 with h₁ | h₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
inl : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
inl₁ : ∀ (h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
rcases h_2 with h₂ | h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
inr : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
inr₁ : ∀ (h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
rcases h_2 with h₂ | h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inl₂ inl₃ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆

Tactic:
rw [h₁, h₂, h]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl₂ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl₃ inl₄ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
rw [h₁, h₂, h, neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
inr₁ : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inr₂ inr₃ : -(↑(∠ p₄ p₅ p₆) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
rw [h₁, h₂, h]