Theorem: one_implies_two
Proof state before:
case intro.mk.mk.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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V) (h₁ : NotCollinear a b c)
    (h₂ :
      ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'),
    ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ 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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
⊢ (a b c : V) →
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        MetricSpace V
Tactic:
refine cont a b c hab ?_ ?_ h₁
Proof state after:
case intro.mk.mk.intro.inr.refine_1
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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ SimpleEdges.Adj b c

case intro.mk.mk.intro.inr.refine_2
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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ SimpleEdges.Adj c a