Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_2.e'_6
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂

pp: case e'_2.e'_7
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂

pp: case e'_3.e'_6
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃

pp: case e'_3.e'_7
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₃ -ᵥ p₁) = p₁ -ᵥ p₃

Tactic:
<;>

Goal state after:
case e'_2.e'_6
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂

case e'_2.e'_7
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂

case e'_3.e'_6
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃

case e'_3.e'_7
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 2 • o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ -(p₃ -ᵥ p₁) = p₁ -ᵥ p₃