V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, r < 0 ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π
rw [angle, angle_eq_pi_iff]
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, r < 0 ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, r < 0 ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
rcases h with ⟨⟨r, ⟨hr0, hr1⟩, hp₂⟩, hp₂p₁, hp₂p₃⟩
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, r < 0 ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
refine' ⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, _⟩
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have hr0' : r ≠ 0 := by
  rintro rfl
  rw [← hp₂] at hp₂p₁
  simp at hp₂p₁
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have hr1' : r ≠ 1 := by
  rintro rfl
  rw [← hp₂] at hp₂p₃
  simp at hp₂p₃
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
replace hr0 := hr0.lt_of_ne hr0'.symm
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ 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₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
replace hr1 := hr1.lt_of_ne hr1'
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ 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₂)
refine' ⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) hr0, _⟩
no goals
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
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]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 0 = p₂
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ r ≠ 0
rintro rfl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : ↑(AffineMap.lineMap p₁ p₃) 0 ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 0 = p₂
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 0 = p₂
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ False
rw [← hp₂] at hp₂p₁
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : ↑(AffineMap.lineMap p₁ p₃) 0 ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 0 = p₂
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ False
simp at hp₂p₁
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : ↑(AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
⊢ r ≠ 1
rintro rfl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : ↑(AffineMap.lineMap p₁ p₃) 1 ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False
rw [← hp₂] at hp₂p₃
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : ↑(AffineMap.lineMap p₁ p₃) 1 ≠ p₃
hp₂ : ↑(AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False
simp at hp₂p₃