simp [*, hl.close_left h.2.1 h.2.2 hacd]
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : b ∈ l ∧ c ∈ l ∧ d ∈ l
⊢ {a, b, c} ⊆ l
no goals