wlog acd : sbtw a c d generalizing a c
case intro.mk.mk.intro.intro.intro
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
a b 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}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
⊢ False
case intro.mk.mk.intro.intro.intro.inr
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
a b 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}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
this :
  ∀ (a c : V),
    SimpleTriangle a b c →
      (∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') →
        Line a c ≠ {a, c} → d ∈ Line a c → sbtw d a c ∨ sbtw a c d → sbtw a c d → False
acd : ¬sbtw a c d
⊢ False

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
hd' : sbtw d a c ∨ sbtw a c d
acd : sbtw a c d
⊢ False