have hbcd : NotCollinear b c d := by
  refine ⟨habc.2.1.ne, h.ne, hcd.ne, fun l hl h ↦ ?_⟩
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
    forall_eq] at h
  refine habc.2.2.2.2.2.2 l hl (by 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
⊢ False
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
hbcd : NotCollinear b c d
⊢ False