simp [right_extend_mem_Line hd] at this
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d ∈ Line a c
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
this : ¬{a, b, c} ⊆ Line a c
⊢ False
no goals