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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
⊢ ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)

Tactic:
have hsp : ∀ p : P × P × P, p ∈ sp → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π := by
    intro p hp
    simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
    obtain ⟨p', hp', rfl⟩ := hp
    dsimp only
    rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
    exact affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
⊢ (p₁, p₃, p₂) ∈ sp

Tactic:
have hp₃ : (p₁, p₃, p₂) ∈ sp :=
    Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₃ : (p₁, p₃, p₂) ∈ sp
⊢ (p₁, p₄, p₂) ∈ sp

Tactic:
have hp₄ : (p₁, p₄, p₂) ∈ sp := Set.mem_image_of_mem _ 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₃ : (p₁, p₃, p₂) ∈ sp
hp₄ : (p₁, p₄, p₂) ∈ sp
⊢ (∡ (p₁, p₄, p₂).1 (p₁, p₄, p₂).2.1 (p₁, p₄, p₂).2.2).sign = (∡ (p₁, p₃, p₂).1 (p₁, p₃, p₂).2.1 (p₁, p₃, p₂).2.2).sign

Tactic:
Real.Angle.sign_eq_of_continuousOn hc hf hsp hp₃ hp₄

Premises used: Real.Angle.sign_eq_of_continuousOn
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₃ : (p₁, p₃, p₂) ∈ sp
hp₄ : (p₁, p₄, p₂) ∈ sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
convert! Real.Angle.sign_eq_of_continuousOn hc hf hsp hp₃ hp₄

Premises used: Real.Angle.sign_eq_of_continuousOn
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₁ p₄
⊢ False

Tactic:
hp₃p₄.left_notMem hp₁

Premises used: AffineSubspace.SOppSide.left_notMem
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₁ p₄
⊢ False

Tactic:
exact hp₃p₄.left_notMem hp₁

Premises used: AffineSubspace.SOppSide.left_notMem
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
⊢ p₁ ≠ p₃

Tactic:
have hp₁p₃ : p₁ ≠ p₃ := by rintro rfl; exact hp₃p₄.left_notMem hp₁
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
rw₁ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign
rw₂ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₃ p₂ p₁).sign
rw₃ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) 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 [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]

Premises used: EuclideanGeometry.oangle_swap₁₃_sign, Real, AffineSubspace.SOppSide.symm, EuclideanGeometry.oangle_rotate_sign, Sbtw.oangle_sign_eq, sbtw_pointReflection_of_ne, AffineSubspace.SSameSide.oangle_sign_eq, AffineSubspace.SOppSide.left_notMem, AffineSubspace.SOppSide.trans, AffineSubspace.sOppSide_pointReflection, 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₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
simp_rw :
  Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔
    Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
⊢ ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
simp_rw [angle, oangle,
    o.angle_eq_iff_oangle_eq_or_sameRay (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)]

Premises used: EuclideanGeometry.oangle, Iff.mpr, vsub_ne_zero, Orientation.angle_eq_iff_oangle_eq_or_sameRay, 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔
    Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
apply or_congr_right

Premises used: or_congr_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : ∀ (h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)), Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
h₁ : ∀ (h : Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
refine ⟨fun h ↦ ?_, fun 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
h₁ : ∀ (r : ℝ) (hr : 0 < r) (he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂), Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
obtain ⟨r, hr, he⟩ := h.exists_pos_left (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)

Premises used: Iff.mpr, vsub_ne_zero, SameRay.exists_pos_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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
h₁ : Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
rw [← vsub_vadd p₁ p₂, ← vsub_vadd p₄ p₂, ← he]

Premises used: vsub_vadd
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
h₁ :
  Wbtw ℝ p₂ (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨
    Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂)
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)

Tactic:
nth_rw 1 4 [← 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₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨
    Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂)

Tactic:
wbtw_or_wbtw_smul_vadd_of_nonneg _ _ zero_le_one hr.le

Premises used: LT.lt.le, zero_le_one, wbtw_or_wbtw_smul_vadd_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨
    Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂)

Tactic:
exact wbtw_or_wbtw_smul_vadd_of_nonneg _ _ zero_le_one hr.le

Premises used: LT.lt.le, zero_le_one, wbtw_or_wbtw_smul_vadd_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
h₁ : ∀ (h : Wbtw ℝ p₂ p₁ p₄), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
h₂ : ∀ (h : Wbtw ℝ p₂ p₄ p₁), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

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

Tactic:
h.sameRay_vsub_left

Premises used: Wbtw.sameRay_vsub_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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₁ p₄
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

Tactic:
exact h.sameRay_vsub_left

Premises used: Wbtw.sameRay_vsub_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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₄ p₁
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

Tactic:
h.sameRay_vsub_left.symm

Premises used: Wbtw.sameRay_vsub_left, SameRay.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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₄ p₁
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)

Tactic:
exact h.sameRay_vsub_left.symm

Premises used: Wbtw.sameRay_vsub_left, SameRay.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₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.left_notMem
-- 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₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.left_notMem
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SSameSide.right_notMem, right_mem_affineSpan_pair
-- 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₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SSameSide.right_notMem, right_mem_affineSpan_pair
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
⊢ (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2

Tactic:
rw [← ha, add_self_div_two] at this

Premises used: add_self_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₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
rw : |(∡ p₁ p₂ p₄).toReal| / |2| = |(∡ p₁ p₂ p₄).toReal| / 2
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2

Tactic:
rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]

Premises used: abs_div, EuclideanGeometry.angle_eq_abs_oangle_toReal
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
⊢ |(∡ p₁ p₂ p₄).toReal| / |2| = |(∡ p₁ p₂ p₄).toReal| / 2

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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
suffices : ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2

Tactic:
suffices ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2 by
    rw [← ha, add_self_div_two] at this
    rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]
    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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄

Tactic:
have hadd := oangle_add 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
⊢ Ne (α := ℝ) 2 0

Tactic:
norm_num
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
rw : (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal
⊢ ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2

Tactic:
rw [div_left_inj' (by norm_num), ← hadd]

Premises used: div_left_inj'
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ Membership.mem (γ := Set P) {p₁, p₂, p₃} p₁

Tactic:
grind
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ Membership.mem (γ := Set P) {p₁, p₂, p₃} p₂

Tactic:
grind
-- 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₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ Membership.mem (γ := Set P) {p₁, p₂, p₃} p₃

Tactic:
grind