V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = π
heq : dist p1 p2 = 0
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = π
⊢ dist p1 p2 ≠ 0
by_contra heq
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = π
heq : p1 = p2
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = π
heq : dist p1 p2 = 0
⊢ False
rw [dist_eq_zero] at heq
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : π / 2 = π
heq : p1 = p2
⊢ False
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = π
heq : p1 = p2
⊢ False
rw [heq, angle_eq_left] at h
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : π / 2 = π
heq : p1 = p2
⊢ False
exact Real.pi_ne_zero (by linarith)
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : π / 2 = π
heq : p1 = p2
⊢ π = 0
linarith