awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
v v₁ v₂ v₃ : V
⊢ ∠ (v - v₁) (v - v₂) (v - v₃) = ∠ v₁ v₂ v₃

Tactic:
simpa only [vsub_eq_sub] using angle_const_vsub v v₁ v₂ v₃

Premises used: EuclideanGeometry.angle_const_vsub, vsub_eq_sub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
v₁ v₂ v₃ : V
⊢ ∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃

Tactic:
simpa only [zero_sub] using angle_const_sub 0 v₁ v₂ v₃

Premises used: EuclideanGeometry.angle_const_sub, OfNat.ofNat, zero_sub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₁

Tactic:
angle_comm _ _

Premises used: InnerProductGeometry.angle_comm, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
⊢ 0 ≤ ∠ p₁ p₂ p₃

Tactic:
angle_nonneg _ _

Premises used: InnerProductGeometry.angle_nonneg, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ ≤ π

Tactic:
angle_le_pi _ _

Premises used: InnerProductGeometry.angle_le_pi, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₀ p : P
rw : InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2
⊢ InnerProductGeometry.angle (p₀ -ᵥ p₀) (p -ᵥ p₀) = π / 2

Tactic:
rw [vsub_self]

Premises used: vsub_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₀ p : P
⊢ InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2

Tactic:
angle_zero_left _

Premises used: InnerProductGeometry.angle_zero_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₀ p : P
⊢ InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2

Tactic:
exact angle_zero_left _

Premises used: InnerProductGeometry.angle_zero_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₀ p : P
rw : ∠ p₀ p₀ p = π / 2
rw₁ rw₂ : π / 2 = π / 2
⊢ ∠ p p₀ p₀ = π / 2

Tactic:
rw [angle_comm, angle_self_left]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_self_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p p₀ : P
h : p ≠ p₀
⊢ ∠ p p₀ p = 0

Tactic:
angle_self <| vsub_ne_zero.2 h

Premises used: Iff.mpr, vsub_ne_zero, InnerProductGeometry.angle_self, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)

Tactic:
rw [angle_eq_pi_iff] at h

Premises used: InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
rcases : ∀ (hp₁p₂ : p₁ -ᵥ p₂ ≠ 0) (r : ℝ) (hr : r < 0) (hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)), ∠ p₂ p₁ p₃ = 0
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
rcases h with ⟨hp₁p₂, ⟨r, ⟨hr, hpr⟩⟩⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
rw : p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) = 0

Tactic:
rw [angle_eq_zero_iff]

Premises used: InnerProductGeometry.angle_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
rw :
  ∀ (hp₁p₂ : p₂ -ᵥ p₁ ≠ 0) (r : ℝ) (hr : r < 0) (hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)),
    p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)

Tactic:
rw [← neg_vsub_eq_vsub_rev, neg_ne_zero] at hp₁p₂

Premises used: neg_vsub_eq_vsub_rev, neg_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
right : p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)

Tactic:
use hp₁p₂, -r + 1, add_pos (neg_pos_of_neg hr) zero_lt_one

Premises used: add_pos, neg_pos_of_neg, zero_lt_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
right : p₃ -ᵥ p₁ = -(-r • (p₁ -ᵥ p₂)) + HSMul.hSMul (α := ℝ) 1 (-(p₁ -ᵥ p₂))
⊢ p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)

Tactic:
rw [add_smul, ← neg_vsub_eq_vsub_rev p₁ p₂, smul_neg]

Premises used: smul_neg, add_smul, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = -(-r • (p₁ -ᵥ p₂)) + HSMul.hSMul (α := ℝ) 1 (-(p₁ -ᵥ p₂))

Tactic:
simp [← hpr]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ ∠ p₃ p₂ p₁ = π

Tactic:
rw [angle_comm] at h

Premises used: EuclideanGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₃ p₂ p₁ = π
⊢ ∠ p₂ p₃ p₁ = 0

Tactic:
angle_eq_zero_of_angle_eq_pi_left h

Premises used: EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₃ p₂ p₁ = π
⊢ ∠ p₂ p₃ p₁ = 0

Tactic:
exact angle_eq_zero_of_angle_eq_pi_left h

Premises used: EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
rcases :
  p₂ -ᵥ p₃ ≠ 0 →
    ∀ (r : ℝ) (hr : r < 0) (hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)),
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

Tactic:
rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, hpr⟩⟩⟩

Premises used: Iff.mp, InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
rw : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) ((-r + 1) • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
angle_smul_right_of_pos (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) (add_pos (neg_pos_of_neg hr) zero_lt_one)

Premises used: InnerProductGeometry.angle_smul_right_of_pos, add_pos, neg_pos_of_neg, VSub.vsub, zero_lt_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
h₁ : p₄ -ᵥ p₂ = (-r + 1) • (p₃ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
convert! angle_smul_right_of_pos (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) (add_pos (neg_pos_of_neg hr) zero_lt_one)

Premises used: InnerProductGeometry.angle_smul_right_of_pos, add_pos, neg_pos_of_neg, VSub.vsub, zero_lt_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
h₁ : p₄ -ᵥ p₂ = - -(p₄ -ᵥ p₃) + HSMul.hSMul (α := ℝ) 1 (-(p₂ -ᵥ p₃))
⊢ p₄ -ᵥ p₂ = (-r + 1) • (p₃ -ᵥ p₂)

Tactic:
rw [add_smul, ← neg_vsub_eq_vsub_rev p₂ p₃, smul_neg, neg_smul, ← hpr]

Premises used: neg_smul, smul_neg, add_smul, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ p₄ -ᵥ p₂ = - -(p₄ -ᵥ p₃) + HSMul.hSMul (α := ℝ) 1 (-(p₂ -ᵥ p₃))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
rw : ∠ p₂ p₃ p₁ + ∠ p₄ p₃ p₁ = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Tactic:
rw [angle_comm p₁ p₃ p₂, angle_comm p₁ p₃ p₄]

Premises used: EuclideanGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) + InnerProductGeometry.angle (p₄ -ᵥ p₃) (p₁ -ᵥ p₃) = π

Tactic:
angle_add_angle_eq_pi_of_angle_eq_pi _ h

Premises used: InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) + InnerProductGeometry.angle (p₄ -ᵥ p₃) (p₁ -ᵥ p₃) = π

Tactic:
exact angle_add_angle_eq_pi_of_angle_eq_pi _ h

Premises used: EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ p₅ : P
hapc : ∠ p₁ p₅ p₃ = π
hbpd : ∠ p₂ p₅ p₄ = π
linarith :
  ∠ p₁ p₅ p₂ < ∠ p₃ p₅ p₄ →
    ∠ p₁ p₅ p₂ - ∠ p₃ p₅ p₄ + -(∠ p₁ p₅ p₂ + ∠ p₁ p₅ p₄ - π) + -(∠ p₄ p₅ p₁ - ∠ p₁ p₅ p₄) +
          (∠ p₄ p₅ p₁ + ∠ p₄ p₅ p₃ - π) +
        -(∠ p₄ p₅ p₃ - ∠ p₃ p₅ p₄) =
      0
linarith₁ :
  ∠ p₃ p₅ p₄ < ∠ p₁ p₅ p₂ →
    ∠ p₃ p₅ p₄ - ∠ p₁ p₅ p₂ + (∠ p₁ p₅ p₂ + ∠ p₁ p₅ p₄ - π) + (∠ p₄ p₅ p₁ - ∠ p₁ p₅ p₄) +
          -(∠ p₄ p₅ p₁ + ∠ p₄ p₅ p₃ - π) +
        (∠ p₄ p₅ p₃ - ∠ p₃ p₅ p₄) =
      0
⊢ ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄

Tactic:
linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
    angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ p₃]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
by_contra : ∀ (heq : dist p₁ p₂ = 0), False
⊢ dist p₁ p₂ ≠ 0

Tactic:
by_contra heq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : dist p₁ p₂ = 0
⊢ p₁ = p₂

Tactic:
rw [dist_eq_zero] at heq

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
⊢ π / 2 = π

Tactic:
rw [heq, angle_self_left] at h

Premises used: EuclideanGeometry.angle_self_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
h₁ : π / 2 = π
⊢ p₁ = p₂

Tactic:
rw [heq, angle_self_left] at h

Premises used: EuclideanGeometry.angle_self_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
linarith₄ : 0 < π → 2 / 2 = 1
linarith₅ : 0 < π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 0 < π → GT.gt (α := ℝ) 2 0
linarith₇ : 0 < π → -(1 * π - 2 * π) + (0 - π) = 0
⊢ π = 0

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ False

Tactic:
exact Real.pi_ne_zero (by linarith)

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ dist p₃ p₂ ≠ 0

Tactic:
left_dist_ne_zero_of_angle_eq_pi <| (angle_comm _ _ _).trans h

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi, Eq.trans
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖
p₄ : P
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Premises used: vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖

Tactic:
norm_sub_eq_add_norm_of_angle_eq_pi h

Premises used: InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π
p₄ : P
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Premises used: vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π

Tactic:
norm_sub_eq_add_norm_iff_angle_eq_pi (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he)) fun he =>
      hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Premises used: vsub_eq_zero_iff_eq, InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi, Iff.mp, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|
p₄ : P
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Premises used: vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|

Tactic:
norm_sub_eq_abs_sub_norm_of_angle_eq_zero h

Premises used: InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0
p₄ : P
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ ∠ p₁ p₂ p₃ = 0

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Premises used: vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

Tactic:
norm_sub_eq_abs_sub_norm_iff_angle_eq_zero (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he))
      fun he => hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Premises used: vsub_eq_zero_iff_eq, InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero, Iff.mp, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
simp : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π
⊢ ∠ p₁ (midpoint ℝ p₁ p₂) p₂ = π

Tactic:
simp only [angle, left_vsub_midpoint, invOf_eq_inv, right_vsub_midpoint, inv_pos, zero_lt_two,
    angle_smul_right_of_pos, angle_smul_left_of_pos]

Premises used: InnerProductGeometry.angle_smul_right_of_pos, inv_pos, invOf_eq_inv, zero_lt_two, right_vsub_midpoint, EuclideanGeometry.angle, InnerProductGeometry.angle_smul_left_of_pos, left_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
rw : InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π

Tactic:
rw [← neg_vsub_eq_vsub_rev p₁ p₂]

Premises used: neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
hx : p₁ -ᵥ p₂ ≠ 0
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π

Tactic:
apply angle_self_neg_of_nonzero

Premises used: InnerProductGeometry.angle_self_neg_of_nonzero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ p₁ -ᵥ p₂ ≠ 0

Tactic:
simpa only [ne_eq, vsub_eq_zero_iff_eq]

Premises used: vsub_eq_zero_iff_eq, ne_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
⊢ p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)

Tactic:
have h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m) := (vsub_sub_vsub_cancel_right p₃ p₁ m).symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
rw : p₃ -ᵥ p₂ = p₃ -ᵥ m + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₁ : p₃ -ᵥ p₂ = p₃ -ᵥ m + (midpoint ℝ p₁ p₂ -ᵥ p₂)
rw₂ rw₃ : p₃ -ᵥ p₂ = p₃ -ᵥ p₂
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)

Tactic:
rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel, midpoint_vsub_right, left_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)

Tactic:
have h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m) := by
    rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]