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₁ 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:
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)
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]
-- 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_neg_of_angle_eq_of_sign_eq_neg h hs

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_neg_of_angle_eq_of_sign_eq_neg, 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_neg_of_sign_eq_neg (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_neg_of_sign_eq_neg, 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 = 1
⊢ ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)

Tactic:
o.oangle_eq_angle_of_sign_eq_one h

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_angle_of_sign_eq_one, 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 = -1
⊢ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)

Tactic:
o.oangle_eq_neg_angle_of_sign_eq_neg_one h

Premises used: EuclideanGeometry.oangle, EuclideanGeometry.o, EuclideanGeometry.angle, Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one
-- 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₂ = 0 ↔ ∠ p₁ p p₂ = 0

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

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.oangle_eq_zero_iff_angle_eq_zero, 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₃ = (↑π : Real.Angle) ↔ ∠ p₁ p₂ p₃ = π

Tactic:
o.oangle_eq_pi_iff_angle_eq_pi

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_pi_iff_angle_eq_pi, 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₃ = (↑(π / 2) : Real.Angle)
rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, 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₃ = (↑(π / 2) : Real.Angle)
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0

Tactic:
o.inner_eq_zero_of_oangle_eq_pi_div_two h

Premises used: Orientation.inner_eq_zero_of_oangle_eq_pi_div_two, 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
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0

Tactic:
exact o.inner_eq_zero_of_oangle_eq_pi_div_two h

Premises used: Orientation.inner_eq_zero_of_oangle_eq_pi_div_two, 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
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₃ p₂ p₁ = π / 2

Tactic:
rw [angle_comm]

Premises used: EuclideanGeometry.angle_comm
-- 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₃ = (↑(π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
angle_eq_pi_div_two_of_oangle_eq_pi_div_two h

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_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₃ = (↑(π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
exact angle_eq_pi_div_two_of_oangle_eq_pi_div_two h

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_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₃ = (↑(-π / 2) : Real.Angle)
rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, 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₃ = (↑(-π / 2) : Real.Angle)
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0

Tactic:
o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h

Premises used: Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two, 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
h : ∡ p₁ p₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0

Tactic:
exact o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h

Premises used: Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two, 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
h : ∡ p₁ p₂ p₃ = (↑(-π / 2) : Real.Angle)
rw : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₃ p₂ p₁ = π / 2

Tactic:
rw [angle_comm]

Premises used: EuclideanGeometry.angle_comm
-- 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₃ = (↑(-π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two h

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_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₃ = (↑(-π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
exact angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two h

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_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
rw :
  (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₂ p₁ p₃).sign

Tactic:
rw [eq_comm, oangle, oangle, ← o.oangle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
    vsub_sub_vsub_cancel_left p₁ p₃ p₂, ← neg_vsub_eq_vsub_rev p₃ p₂, sub_eq_add_neg,
    neg_vsub_eq_vsub_rev p₂ p₁, add_comm, ← @neg_one_smul ℝ]

Premises used: EuclideanGeometry.oangle, Real, neg_one_smul, sub_eq_add_neg, eq_comm, add_comm, vsub_sub_vsub_cancel_left, 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
nth_rw :
  (Orientation.oangle o (p₁ -ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
⊢ (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
nth_rw 2 [← one_smul ℝ (p₁ -ᵥ p₂)]

Premises used: Real, VSub.vsub, one_smul
-- 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
rw :
  HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-1) : SignType)
      (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
⊢ (Orientation.oangle o (p₁ -ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
rw [o.oangle_sign_smul_add_smul_right]

Premises used: Orientation.oangle_sign_smul_add_smul_right, 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
⊢ HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-1) : SignType)
      (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

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
rw : -(-∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
rw₁ : - -(∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
rw₂ rw₃ : (∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign

Tactic:
rw [oangle_rev, Real.Angle.sign_neg, neg_neg]

Premises used: Real.Angle.sign_neg, EuclideanGeometry.oangle_rev, 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
rw : (∡ p₃ p₂ p₁).sign = (∡ p₁ p₃ p₂).sign
rw₁ : -(∡ p₂ p₃ p₁).sign = (∡ p₁ p₃ p₂).sign
rw₂ rw₃ : (∡ p₁ p₃ p₂).sign = (∡ p₁ p₃ p₂).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign

Tactic:
rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

Premises used: EuclideanGeometry.oangle_swap₁₃_sign, EuclideanGeometry.oangle_swap₁₂_sign
-- 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
rw : -(∡ p₃ p₂ p₁).sign = (∡ p₁ p₂ p₃).sign
rw₁ rw₂ : (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃).sign
⊢ (∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign

Tactic:
rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

Premises used: EuclideanGeometry.oangle_swap₁₃_sign, EuclideanGeometry.oangle_swap₁₂_sign
-- 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
rw : ∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
rw₁ rw₂ : Sbtw ℝ p₁ p₂ p₃ ↔ Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Sbtw ℝ p₁ p₂ p₃

Tactic:
rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]

Premises used: EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi, EuclideanGeometry.angle_eq_pi_iff_sbtw
-- 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 : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = (↑π : Real.Angle)

Tactic:
oangle_eq_pi_iff_sbtw.2 h

Premises used: Iff.mpr, EuclideanGeometry.oangle_eq_pi_iff_sbtw
-- 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 : Sbtw ℝ p₁ p₂ p₃
rw : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
rw₁ rw₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ p₃ p₂ p₁ = (↑π : Real.Angle)

Tactic:
rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]

Premises used: Sbtw.oangle₁₂₃_eq_pi, EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi
-- 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 : Wbtw ℝ p₁ p₂ p₃
pos : ∀ (hp₂p₁ : p₂ = p₁), ∡ p₂ p₁ p₃ = 0
neg : ∀ (hp₂p₁ : ¬p₂ = p₁), ∡ p₂ p₁ p₃ = 0
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
by_cases hp₂p₁ : p₂ = p₁
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
simp [hp₂p₁]
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
pos : ∀ (hp₃p₁ : p₃ = p₁), ∡ p₂ p₁ p₃ = 0
neg : ∀ (hp₃p₁ : ¬p₃ = p₁), ∡ p₂ p₁ p₃ = 0
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
by_cases hp₃p₁ : p₃ = p₁
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
simp [hp₃p₁]
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
neg : ∠ p₂ p₁ p₃ = 0
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
rw [oangle_eq_zero_iff_angle_eq_zero hp₂p₁ hp₃p₁]

Premises used: EuclideanGeometry.oangle_eq_zero_iff_angle_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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
h.angle₂₁₃_eq_zero_of_ne hp₂p₁

Premises used: Wbtw.angle₂₁₃_eq_zero_of_ne
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
exact h.angle₂₁₃_eq_zero_of_ne hp₂p₁

Premises used: Wbtw.angle₂₁₃_eq_zero_of_ne
-- 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 : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
h.wbtw.oangle₂₁₃_eq_zero

Premises used: Wbtw.oangle₂₁₃_eq_zero, Sbtw.wbtw
-- 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 : Wbtw ℝ p₁ p₂ p₃
rw : ∡ p₂ p₁ p₃ = 0
rw₁ rw₂ : Eq (α := Real.Angle) 0 0
⊢ ∡ p₃ p₁ p₂ = 0

Tactic:
rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_zero]

Premises used: Wbtw.oangle₂₁₃_eq_zero, EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_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 : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₁ p₂ = 0

Tactic:
h.wbtw.oangle₃₁₂_eq_zero

Premises used: Wbtw.oangle₃₁₂_eq_zero, Sbtw.wbtw
-- 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 : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₃ p₁ = 0

Tactic:
h.symm.oangle₂₁₃_eq_zero

Premises used: Wbtw.oangle₂₁₃_eq_zero, Wbtw.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
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₃ p₁ = 0

Tactic:
h.wbtw.oangle₂₃₁_eq_zero

Premises used: Wbtw.oangle₂₃₁_eq_zero, Sbtw.wbtw
-- 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 : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₁ p₃ p₂ = 0

Tactic:
h.symm.oangle₃₁₂_eq_zero

Premises used: Wbtw.oangle₃₁₂_eq_zero, Wbtw.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
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₁ p₃ p₂ = 0

Tactic:
h.wbtw.oangle₁₃₂_eq_zero

Premises used: Sbtw.wbtw, Wbtw.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
pos : ∀ (hp₁p₂ : p₁ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
neg : ∀ (hp₁p₂ : ¬p₁ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

Tactic:
by_cases hp₁p₂ : p₁ = p₂
-- 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₁ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

Tactic:
simp [hp₁p₂]
-- 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₁ = p₂
pos : ∀ (hp₃p₂ : p₃ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
neg : ∀ (hp₃p₂ : ¬p₃ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

Tactic:
by_cases hp₃p₂ : p₃ = p₂
-- 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₁ = p₂
hp₃p₂ : p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

Tactic:
simp [hp₃p₂]