simp [*, hl.close_middle hl'.1 hl'.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
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
hl' : a ∈ l ∧ b ∈ l ∧ d ∈ l
⊢ {a, b, c} ⊆ l
no goals