awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
r : ℝ
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
⊢ r ≠ 0

Tactic:
have hr0' : r ≠ 0 := by
    rintro rfl
    simp at hp₂p₁
-- 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
r : ℝ
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
⊢ 0 < r

Tactic:
replace hr0 := hr0.lt_of_ne hr0'.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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)

Tactic:
⟨vsub_ne_zero.2 hp₂p₁, r⁻¹, inv_pos.2 hr0, ?_⟩

Premises used: Iff.mpr, vsub_ne_zero, inv_pos, Inv.inv, And.intro, Exists.intro
-- 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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
refine : p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)

Tactic:
refine ⟨vsub_ne_zero.2 hp₂p₁, r⁻¹, inv_pos.2 hr0, ?_⟩
-- 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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
rw₃ : p₃ -ᵥ p₁ = r⁻¹ • r • (p₃ -ᵥ p₁)
rw₄ : p₃ -ᵥ p₁ = (r⁻¹ * r) • (p₃ -ᵥ p₁)
rw₅ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
rw₆ rw₇ : p₃ -ᵥ p₁ = p₃ -ᵥ p₁
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)

Tactic:
rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]

Premises used: vadd_vsub_assoc, smul_smul, one_smul, AffineMap.lineMap_apply, add_zero, inv_mul_cancel₀, 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₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
h.wbtw.angle₂₁₃_eq_zero_of_ne h.ne_left

Premises used: Sbtw.ne_left, Wbtw.angle₂₁₃_eq_zero_of_ne, Sbtw.wbtw
-- 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
rw : ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃
rw₁ rw₂ : ∠ p₂ p₁ p₃ = ∠ p₂ p₁ p₃
⊢ ∠ p₃ p₁ p₂ = 0

Tactic:
rw [← h.angle₂₁₃_eq_zero_of_ne hp₂p₁, angle_comm]

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

Tactic:
h.wbtw.angle₃₁₂_eq_zero_of_ne h.ne_left

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

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

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

Tactic:
h.wbtw.angle₂₃₁_eq_zero_of_ne h.ne_right

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

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

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

Tactic:
h.wbtw.angle₁₃₂_eq_zero_of_ne h.ne_right

Premises used: Wbtw.angle₁₃₂_eq_zero_of_ne, Sbtw.wbtw, Sbtw.ne_right
-- 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
mp : ∠ p₁ p₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
mpr : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ → ∠ p₁ p₂ p₃ = 0
⊢ ∠ p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
constructor
-- 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
mp :
  (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
rw [angle, angle_eq_zero_iff]

Premises used: InnerProductGeometry.angle_eq_zero_iff, 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
mp : ∀ (hr1 : 1 ≤ r), p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
mp₁ : ∀ (hr1 : r < 1), p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
rcases le_or_gt 1 r with (hr1 | hr1)

Premises used: le_or_gt, OfNat.ofNat
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
Or.inl ⟨vsub_ne_zero.1 hp₁p₂, r⁻¹, ⟨(inv_pos.2 hr0).le, inv_le_one_of_one_le₀ hr1⟩, ?_⟩

Premises used: Iff.mpr, vsub_ne_zero, inv_pos, LT.lt.le, Inv.inv, And.intro, Exists.intro, Iff.mp, Or.inl, inv_le_one_of_one_le₀
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
refine Or.inl ⟨vsub_ne_zero.1 hp₁p₂, r⁻¹, ⟨(inv_pos.2 hr0).le, inv_le_one_of_one_le₀ hr1⟩, ?_⟩

Premises used: Or.inl
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₂ : (r⁻¹ * r) • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₃ : HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₄ : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₅ mp₆ : p₁ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁

Tactic:
rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]

Premises used: smul_smul, Ne.symm, one_smul, AffineMap.lineMap_apply, vsub_vadd, inv_mul_cancel₀, LT.lt.ne
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩

Premises used: LT.lt.le, And.intro, Exists.intro, Or.inr
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : p₃ ≠ p₂
mp₁ : (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
refine Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩

Premises used: Or.inr
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
⊢ p₃ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]

Premises used: vsub_ne_zero, smul_ne_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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

Tactic:
⟨hr0.ne.symm, hp₁p₂⟩

Premises used: Ne.symm, And.intro, LT.lt.ne
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

Tactic:
exact ⟨hr0.ne.symm, hp₁p₂⟩
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₃
mp₁ : (p₃ -ᵥ p₂) +ᵥ p₂ = p₃
mp₂ mp₃ : p₃ = p₃
⊢ (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃

Tactic:
rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]

Premises used: AffineMap.lineMap_apply, vsub_vadd
-- 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₂
h : Wbtw ℝ 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.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₂
h : Wbtw ℝ 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.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₂
h : Wbtw ℝ 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.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₂
h : Wbtw ℝ 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.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
rw : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

Tactic:
rw [angle_eq_zero_iff_ne_and_wbtw]

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

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

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

Tactic:
by_cases hp₁p₃ : p₁ = p₃
-- 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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

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

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

Tactic:
simp [hp₃p₂]
-- 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₃
hp₃p₂ : ¬p₃ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

Tactic:
simp [hp₁p₂, hp₁p₃, Ne.symm hp₁p₃, Sbtw, hp₃p₂]

Premises used: Ne.symm, Sbtw
-- 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 : Sbtw ℝ p₂ p₃ p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p

Tactic:
angle_eq_angle_of_angle_eq_pi _ h.angle₁₂₃_eq_pi

Premises used: EuclideanGeometry.angle_eq_angle_of_angle_eq_pi, Sbtw.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 : Sbtw ℝ p₂ p₁ p
⊢ ∠ p₁ p₂ p₃ = ∠ p p₂ p₃

Tactic:
simpa only [angle_comm] using h.angle_eq_right p₃

Premises used: EuclideanGeometry.angle_comm, Sbtw.angle_eq_right
-- 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 : 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.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 : 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.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 : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
hp₃p : ¬p₃ = p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p

Tactic:
Sbtw.angle_eq_right _ ⟨h, hp₃p₂, hp₃p⟩

Premises used: Sbtw.angle_eq_right, And.intro
-- 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 : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
hp₃p : ¬p₃ = p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p

Tactic:
exact Sbtw.angle_eq_right _ ⟨h, hp₃p₂, hp₃p⟩

Premises used: Sbtw.angle_eq_right, And.intro
-- 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 : Wbtw ℝ p₂ p₁ p
hp₁p₂ : p₁ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = ∠ p p₂ p₃

Tactic:
simpa only [angle_comm] using h.angle_eq_right p₃ hp₁p₂

Premises used: EuclideanGeometry.angle_comm, Wbtw.angle_eq_right
-- 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
pos : ∀ (h₃₂ : p₃ = p₂), ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
neg : ∀ (h₃₂ : p₃ ≠ p₂), ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
by_cases! h₃₂ : p₃ = p₂
-- 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₂
pos : π / 2 = π - π / 2
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
simp [h₃₂]
-- 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₂
⊢ π / 2 = π - π / 2

Tactic:
field
-- 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₂
neg : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) + ∠ p₁ p₂ p₃ = π
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
rw [eq_sub_iff_add_eq]

Premises used: eq_sub_iff_add_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₃₂ : p₃ ≠ p₂
neg : ∠ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₃ = π
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) + ∠ p₁ p₂ p₃ = π

Tactic:
apply EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi

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

Tactic:
Sbtw.angle₁₂₃_eq_pi <| (sbtw_pointReflection_of_ne ℝ h₃₂.symm).symm

Premises used: Real, Ne.symm, sbtw_pointReflection_of_ne, Sbtw.angle₁₂₃_eq_pi, Sbtw.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₃₂ : p₃ ≠ p₂
⊢ ∠ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₃ = π

Tactic:
exact Sbtw.angle₁₂₃_eq_pi <| (sbtw_pointReflection_of_ne ℝ h₃₂.symm).symm

Premises used: Real, Ne.symm, sbtw_pointReflection_of_ne, Sbtw.angle₁₂₃_eq_pi, Sbtw.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
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : Collinear ℝ (P := P) {p₁, p₂, p₃}), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
refine_2 : ∀ (h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- 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 : Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂

Tactic:
replace h := h.wbtw_or_wbtw_or_wbtw