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₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ let m := midpoint ℝ p₁ p₂;
  ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖

Tactic:
rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h

Premises used: 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 : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
h₁ :
  let m := midpoint ℝ p₁ p₂;
  ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
⊢ let m := midpoint ℝ p₁ p₂;
  p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)

Tactic:
rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h

Premises used: 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 : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
h₁ :
  let m := midpoint ℝ p₁ p₂;
  ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1₁ :
  let m := midpoint ℝ p₁ p₂;
  p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ let m := midpoint ℝ p₁ p₂;
  p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)

Tactic:
rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h

Premises used: 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
m : P := midpoint ℝ p₁ p₂
h : ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
(norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p₃ -ᵥ m) (p₁ -ᵥ m)).mp h.symm

Premises used: InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, VSub.vsub, Iff.mp, Eq.symm, 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
m : P := midpoint ℝ p₁ p₂
h : ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
exact (norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p₃ -ᵥ m) (p₁ -ᵥ m)).mp h.symm

Premises used: InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, VSub.vsub, Iff.mp, Eq.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₂
rw : ∠ p₃ (midpoint ℝ p₂ p₁) p₂ = π / 2
rw₁ rw₂ : π / 2 = π / 2
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2

Tactic:
rw [midpoint_comm p₁ p₂, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.symm]

Premises used: midpoint_comm, EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq, Eq.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₃
rw : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₁ p₂ p₃ = π

Tactic:
rw [angle, angle_eq_pi_iff]

Premises used: InnerProductGeometry.angle_eq_pi_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
h : Sbtw ℝ p₁ p₂ p₃
rcases :
  ∀ (r : ℝ) (hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hp₂p₁ : p₂ ≠ p₁)
    (hp₂p₃ : p₂ ≠ p₃), p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)

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

Tactic:
⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, ?_⟩

Premises used: Iff.mpr, vsub_ne_zero, HSub.hSub, HDiv.hDiv, Ne.symm, And.intro, Exists.intro, OfNat.ofNat, Neg.neg
-- 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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
refine : -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)

Tactic:
refine ⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, ?_⟩
-- 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₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
hp₂p₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
⊢ p₂ ≠ p₃

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
hp₂p₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
hp₂p₄ : p₂ ≠ p₃
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
hp₂p₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
hp₂p₄ : p₂ ≠ p₃
hp₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
⊢ LE.le (α := ℝ) 0 0

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
hp₂p₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
hp₂p₄ : p₂ ≠ p₃
hp₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0₁ : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
⊢ False

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

Tactic:
have hr0' : r ≠ 0 := by
    rintro rfl
    rw [← hp₂] at hp₂p₁
    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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
hp₂p₄ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
hp₂p₄ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
hp₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
⊢ LE.le (α := ℝ) 0 1

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
hp₂p₄ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
hp₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0₁ : LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 1 1

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
hp₂p₄ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
hp₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0₁ : LE.le (α := ℝ) 0 1
hr1₁ : LE.le (α := ℝ) 1 1
⊢ Ne (α := ℝ) 1 0

Tactic:
rw [← hp₂] 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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
⊢ False

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

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

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

Tactic:
⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) hr0, ?_⟩

Premises used: Iff.mpr, sub_pos, Left.neg_neg_iff, And.intro, div_neg_of_neg_of_pos
-- 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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
refine : p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)

Tactic:
refine ⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) 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₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
rw₁₁ : p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)
rw₁₂ : p₃ -ᵥ p₁ = (1 - r + r) • (p₃ -ᵥ p₁)
rw₁₃ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
rw₁₄ rw₁₅ : p₃ -ᵥ p₁ = p₃ -ᵥ p₁
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)

Tactic:
rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]

Premises used: div_mul_cancel₀, neg_smul, vsub_vadd_eq_vsub_sub, smul_smul, neg_neg, smul_neg, one_smul, AffineMap.lineMap_apply, add_smul, sub_eq_iff_eq_add, sub_add_cancel, vsub_self, 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
h : Sbtw ℝ p₁ p₂ p₃
rw : ∠ p₃ p₂ p₁ = ∠ p₁ p₂ p₃
rw₁ rw₂ : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃
⊢ ∠ p₃ p₂ p₁ = π

Tactic:
rw [← h.angle₁₂₃_eq_pi, angle_comm]

Premises used: EuclideanGeometry.angle_comm, 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₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃

Tactic:
⟨?_, fun h => h.angle₁₂₃_eq_pi⟩

Premises used: Sbtw.angle₁₂₃_eq_pi, 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 : ∠ p₁ p₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃

Tactic:
refine ⟨?_, fun h => h.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
rw : (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃

Tactic:
rw [angle, angle_eq_pi_iff]

Premises used: InnerProductGeometry.angle_eq_pi_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 : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ Sbtw ℝ p₁ p₂ p₃

Tactic:
⟨⟨1 / (1 - r), ⟨div_nonneg zero_le_one (sub_nonneg.2 (hr.le.trans zero_le_one)),
    (div_le_one (sub_pos.2 (hr.trans zero_lt_one))).2 ((le_sub_self_iff 1).2 hr.le)⟩, ?_⟩,
    (vsub_ne_zero.1 hp₁p₂).symm, ?_⟩

Premises used: Iff.mpr, sub_pos, vsub_ne_zero, HSub.hSub, HDiv.hDiv, LT.lt.le, Ne.symm, zero_le_one, zero_lt_one, div_le_one, le_sub_self_iff, And.intro, Exists.intro, Iff.mp, LT.lt.trans, div_nonneg, LE.le.trans, OfNat.ofNat, sub_nonneg, 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
refine_1 : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂
refine_2 : p₂ ≠ p₃
⊢ Sbtw ℝ p₁ p₂ p₃

Tactic:
refine ⟨⟨1 / (1 - r), ⟨div_nonneg zero_le_one (sub_nonneg.2 (hr.le.trans zero_le_one)),
    (div_le_one (sub_pos.2 (hr.trans zero_lt_one))).2 ((le_sub_self_iff 1).2 hr.le)⟩, ?_⟩,
    (vsub_ne_zero.1 hp₁p₂).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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂

Tactic:
rw [← eq_vadd_iff_vsub_eq] at hp₃p₂

Premises used: eq_vadd_iff_vsub_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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
refine_1 : p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂

Tactic:
rw [AffineMap.lineMap_apply, hp₃p₂, vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev p₂ p₁, smul_neg, ←
      neg_smul, smul_add, smul_smul, ← add_smul, eq_comm, eq_vadd_iff_vsub_eq]

Premises used: neg_smul, vadd_vsub_assoc, smul_smul, smul_neg, eq_comm, AffineMap.lineMap_apply, add_smul, neg_vsub_eq_vsub_rev, eq_vadd_iff_vsub_eq, smul_add
-- 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
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₂ -ᵥ p₁)

Tactic:
(one_smul ℝ (p₂ -ᵥ p₁)).symm

Premises used: Real, VSub.vsub, one_smul, Eq.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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
h : 1 / (1 - r) * -r + 1 / (1 - r) = 1
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)

Tactic:
convert! (one_smul ℝ (p₂ -ᵥ p₁)).symm

Premises used: Real, VSub.vsub, one_smul, Eq.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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ 1 / (1 - r) * -r + 1 / (1 - r) = 1

Tactic:
field [(sub_pos.2 (hr.trans zero_lt_one)).ne.symm]

Premises used: Iff.mpr, sub_pos, Ne.symm, zero_lt_one, LT.lt.trans, 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 : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
refine_2 : r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
⊢ p₂ ≠ p₃

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

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

Tactic:
⟨hr.ne, hp₁p₂⟩

Premises used: 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 : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

Tactic:
exact ⟨hr.ne, 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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
rw : p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
⊢ ∠ p₂ p₁ p₃ = 0

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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
rcases :
  ∀ (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hp₂p₁ : (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₁)
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)

Tactic:
rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩

Premises used: rfl
-- 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
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
⊢ False

Tactic:
simp at hp₂p₁