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
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
neg : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

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

Premises used: EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero, EuclideanGeometry.angle_eq_zero_iff_ne_and_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
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

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

Tactic:
rw [hp₁'p₂, wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- 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
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
h₁ : p₁ = p₂
⊢ p₁ ≠ p₂

Tactic:
rw [hp₁'p₂, wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- 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
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
h₁ : p₁ = p₂
hp₁p₃ : p₁ ≠ p₂
⊢ ¬p₃ = p₂

Tactic:
rw [hp₁'p₂, wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- 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
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
h₁ : p₁ = p₂
hp₁p₃ : p₁ ≠ p₂
hp₃p₃ : ¬p₃ = p₂
⊢ p₁' = p₂

Tactic:
rw [hp₁'p₂, wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- 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
h : p₁ = p₂
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃

Tactic:
False.elim (hp₁p₂ h)

Premises used: False.elim
-- 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
h : p₁ = p₂
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃

Tactic:
exact False.elim (hp₁p₂ h)

Premises used: False.elim
-- 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
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : ¬p₁' = p₂
neg : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₁ + ∡ p₁ p₂ p₃
neg₁ : ∡ p₁ p₂ p₃ = 0 + ∡ p₁ p₂ p₃
neg₂ neg₃ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃

Tactic:
rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]

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

Tactic:
h.wbtw.oangle_eq_left h.ne_left

Premises used: Sbtw.ne_left, Wbtw.oangle_eq_left, 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₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
rw : -∡ p₃ p₂ p₁ = ∡ p₁ p₂ p₃'
rw₁ : -∡ p₃' p₂ p₁ = ∡ p₁ p₂ p₃'
rw₂ rw₃ : ∡ p₁ p₂ p₃' = ∡ p₁ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'

Tactic:
rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]

Premises used: Wbtw.oangle_eq_left, EuclideanGeometry.oangle_rev
-- 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
h : Sbtw ℝ p₂ p₃ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'

Tactic:
h.wbtw.oangle_eq_right h.ne_left

Premises used: Sbtw.ne_left, Sbtw.wbtw, Wbtw.oangle_eq_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
pos : ∀ (h : p₁ = p₂), ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
neg : ∀ (h : ¬p₁ = p₂), ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
by_cases h : 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 : p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
simp [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
h : ¬p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
(sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_left

Premises used: Real, sbtw_midpoint_of_ne, Sbtw.symm, Sbtw.oangle_eq_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₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_left

Premises used: Real, sbtw_midpoint_of_ne, Sbtw.symm, Sbtw.oangle_eq_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
rw : ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
rw₁ rw₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
rw [midpoint_comm, oangle_midpoint_left]

Premises used: midpoint_comm, EuclideanGeometry.oangle_midpoint_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
pos : ∀ (h : p₃ = p₂), ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
neg : ∀ (h : ¬p₃ = p₂), ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
by_cases h : 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 : p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
simp [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
h : ¬p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
(sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right

Premises used: Real, sbtw_midpoint_of_ne, Sbtw.oangle_eq_right, Sbtw.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 : ¬p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right

Premises used: Real, sbtw_midpoint_of_ne, Sbtw.oangle_eq_right, Sbtw.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
rw : ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
rw₁ rw₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃

Tactic:
rw [midpoint_comm, oangle_midpoint_right]

Premises used: EuclideanGeometry.oangle_midpoint_right, midpoint_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₃ : P
h : Sbtw ℝ p₁ p₂ p₁'
hp₃p₂ : p₃ ≠ p₂
rw : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ∡ p₁ p₂ p₁'
rw₁ rw₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + (↑π : Real.Angle)

Tactic:
rw [← h.oangle₁₂₃_eq_pi, oangle_add_swap h.left_ne h.right_ne hp₃p₂]

Premises used: Sbtw.oangle₁₂₃_eq_pi, EuclideanGeometry.oangle_add_swap, Sbtw.right_ne, Sbtw.left_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₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
rw : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ∡ p₃' p₂ p₃
rw₁ rw₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + (↑π : Real.Angle)

Tactic:
rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]

Premises used: EuclideanGeometry.oangle_add, Sbtw.right_ne, Sbtw.oangle₃₂₁_eq_pi, Sbtw.left_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₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₁ : ∡ p₁' p₂ p₃' + (↑π : Real.Angle) + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₂ : ∡ p₁' p₂ p₃' + ((↑π : Real.Angle) + (↑π : Real.Angle)) = ∡ p₁' p₂ p₃'
rw₃ : ∡ p₁' p₂ p₃' + 0 = ∡ p₁' p₂ p₃'
rw₄ rw₅ : ∡ p₁' p₂ p₃' = ∡ p₁' p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'

Tactic:
rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]

Premises used: Sbtw.oangle_eq_add_pi_left, add_assoc, Sbtw.right_ne, Sbtw.oangle_eq_add_pi_right, add_zero, Real.Angle.coe_pi_add_coe_pi, Sbtw.left_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₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
rw : ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₂ : P)
| p₂

Tactic:
rw [← AffineEquiv.pointReflection_self ℝ p₂]

Premises used: Real, AffineEquiv.pointReflection_self
-- 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₂
h₃₂ : p₃ ≠ p₂
conv_rhs :
  Ne (α := P) ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ : P)
    ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₂ : P)
⊢ (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂

Tactic:
conv_rhs => rw [← AffineEquiv.pointReflection_self ℝ p₂]

Premises used: Real, AffineEquiv.pointReflection_self
-- 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₂
h₃₂ rw : p₃ ≠ p₂
⊢ Ne (α := P) ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ : P)
    ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₂ : P)

Tactic:
rw [(AffineEquiv.pointReflection ℝ p₂).injective.ne_iff]

Premises used: Real, Function.Injective.ne_iff, AffineEquiv.injective, AffineEquiv.pointReflection
-- 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₂
h₃₂ : p₃ ≠ p₂
⊢ p₃ ≠ p₂

Tactic:
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
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ p₃ ≠ p₂

Tactic:
exact 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
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂

Tactic:
have h₂₃' : (AffineEquiv.pointReflection ℝ p₂) p₃ ≠ p₂ := by
    conv_rhs => rw [← AffineEquiv.pointReflection_self ℝ p₂]
    rw [(AffineEquiv.pointReflection ℝ p₂).injective.ne_iff]
    exact 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
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
h₂₃' : (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
rw : ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = (↑π : Real.Angle)
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)

Tactic:
rw [← sub_eq_iff_eq_add', oangle_sub_left h₁₂ h₃₂ h₂₃']

Premises used: EuclideanGeometry.oangle_sub_left, sub_eq_iff_eq_add'
-- 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₂
h₃₂ : p₃ ≠ p₂
h₂₃' : (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
⊢ ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = (↑π : Real.Angle)

Tactic:
Sbtw.oangle₁₂₃_eq_pi <| sbtw_pointReflection_of_ne ℝ h₃₂.symm

Premises used: Sbtw.oangle₁₂₃_eq_pi, Real, Ne.symm, sbtw_pointReflection_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₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
h₂₃' : (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
⊢ ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = (↑π : Real.Angle)

Tactic:
exact Sbtw.oangle₁₂₃_eq_pi <| sbtw_pointReflection_of_ne ℝ h₃₂.symm

Premises used: Sbtw.oangle₁₂₃_eq_pi, Real, Ne.symm, sbtw_pointReflection_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₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
rw : ∡ p₁ p₂ p₃ + -(↑π : Real.Angle) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)
⊢ ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₁) p₂ p₃ = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)

Tactic:
rw [oangle_rev, oangle_pointReflection_right h₃₂ h₁₂, neg_add, ← oangle_rev]

Premises used: EuclideanGeometry.oangle_rev, neg_add, EuclideanGeometry.oangle_pointReflection_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
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ + -(↑π : Real.Angle) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)

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
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
pos : ∀ (hp₃p₂ : p₃ = p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg : ∀ (hp₃p₂ : ¬p₃ = p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ 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₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : p₃ = p₂
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ 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₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
neg : ∀ (hw : Wbtw ℝ p₁ p₂ p₁'), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₁ : ∀ (hw : Wbtw ℝ p₂ p₁' p₁), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₂ : ∀ (hw : Wbtw ℝ p₁' p₁ p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)

Tactic:
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)

Premises used: Collinear.wbtw_or_wbtw_or_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₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ Sbtw ℝ p₁ p₂ p₁'

Tactic:
have hw' : Sbtw ℝ p₁ p₂ p₁' := ⟨hw, hp₁p₂.symm, hp₁'p₂.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
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃ + (↑π : Real.Angle)) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (↑π : Real.Angle) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₂ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + 0 = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₃ neg₄ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)

Tactic:
rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]

Premises used: Sbtw.oangle_eq_add_pi_left, Real.Angle.two_zsmul_coe_pi, add_zero, smul_add
-- 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
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
neg neg₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)

Tactic:
rw [hw.oangle_eq_left hp₁'p₂]

Premises used: Wbtw.oangle_eq_left