intro a' b' c' h
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' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
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' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
a' b' c' : V
h : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'