-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_eq_zero_of_angle_eq_pi_left {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) : ∠ p₂ p₁ p₃ = 0

Proof state:
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 : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
rcases h with ⟨hp₁p₂, ⟨r, ⟨hr, hpr⟩⟩⟩

Result:
case 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0

Proof state:
case right
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₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = -(-r • (p₁ -ᵥ p₂)) + 1 • -(p₁ -ᵥ p₂)

Tactic:
simp [← hpr]

Result:
no goals

Proof state:
case 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
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₁)

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

Result:
case right
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₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)

Proof state:
case 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
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₁)

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

Result:
case 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
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₁)

Proof state:
case 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) = 0

Tactic:
rw [angle_eq_zero_iff]

Result:
case 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
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₁)

Proof state:
case right
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₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)

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

Result:
case right
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₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = -(-r • (p₁ -ᵥ p₂)) + 1 • -(p₁ -ᵥ p₂)

Proof state:
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 : ∠ p₁ p₂ p₃ = π
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
unfold angle at h

Result:
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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π
⊢ ∠ p₂ p₁ p₃ = 0

Proof state:
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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
rw [angle_eq_pi_iff] at h

Result:
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 : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0

Proof state:
case 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
unfold angle

Result:
case 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) = 0