Theorem: one_implies_two (LeanCamCombi/SylvesterChvatal.lean)

State before:
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
let S : Set (V × V × V) := setOf (fun ⟨a, b, c⟩ => NotCollinear a b c)
State after:
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}
⊢ ∃ x y z, SimpleTriangle x y z

State before:
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}
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
have : S.Nonempty := let ⟨x, y, z, hxyz⟩ := h; ⟨(x, y, z), hxyz⟩
State after:
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
⊢ ∃ x y z, SimpleTriangle x y z

State before:
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
let f : V × V × V → ℝ := fun ⟨a, b, c⟩ => dist a b + dist b c + dist c a
State after:
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
⊢ ∃ x y z, SimpleTriangle x y z

State before:
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
obtain ⟨⟨a, b, c⟩, (h₁ : NotCollinear _ _ _), h₂⟩ := S.toFinite.exists_minimal_wrt f S this
State after:
case intro.mk.mk.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, 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' ∈ S, f a' ≤ f (a, b, c) → f (a, b, c) = f a'
⊢ ∃ x y z, SimpleTriangle x y z

State before:
case intro.mk.mk.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, 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' ∈ S, f a' ≤ f (a, b, c) → f (a, b, c) = f a'
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
simp only [Prod.forall, Set.mem_setOf_eq] at h₂
State after:
case intro.mk.mk.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, 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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
⊢ ∃ x y z, SimpleTriangle x y z

State before:
case intro.mk.mk.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, 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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
replace 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' := by
  intro a' b' c' hL
  by_contra! h
  exact h.ne' (h₂ a' b' c' hL h.le)
State after:
case intro.mk.mk.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, 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'
⊢ ∃ x y z, SimpleTriangle x y z

State before:
case intro.mk.mk.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, 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'
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
simp only [SimpleTriangle]
State after:
case intro.mk.mk.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, 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'
⊢ ∃ x y z, SimpleEdges.Adj x y ∧ SimpleEdges.Adj y z ∧ SimpleEdges.Adj z x ∧ NotCollinear x y z

State before:
case intro.mk.mk.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, 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'
⊢ ∃ x y z, SimpleEdges.Adj x y ∧ SimpleEdges.Adj y z ∧ SimpleEdges.Adj z x ∧ NotCollinear x y z
Tactic:
by_contra! cont
State after:
case intro.mk.mk.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, 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
⊢ False

State before:
case intro.mk.mk.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, 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
⊢ False
Tactic:
wlog hab : ¬ SimpleEdges.Adj a b generalizing a b c
State after:
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
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'
hab : ¬SimpleEdges.Adj a b
⊢ False

State before:
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
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'
hab : ¬SimpleEdges.Adj a b
⊢ False
Tactic:
simp only [SimpleEdges_adj, h₁.1, ne_eq, not_false_eq_true, true_and, not_forall, not_not] at hab
State after:
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
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'
hab : ∃ x, sbtw a x b
⊢ False

State before:
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
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'
hab : ∃ x, sbtw a x b
⊢ False
Tactic:
obtain ⟨d, adb⟩ := hab
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
⊢ False
Tactic:
have habc : c ∉ Line a b := fun hc ↦ h₁.2.2.2 (Line a b) (Line_isLine h₁.1)
    (by simp [left_mem_Line, right_mem_Line, hc])
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
⊢ False
Tactic:
have hdab : d ∈ Line a b := middle_extend_mem_Line adb
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
⊢ False
Tactic:
have : dist d c < dist d b + dist b c := by
  by_contra!
  refine habc (generateLine_close_right hdab right_mem_Line ?_)
  exact ⟨adb.ne23, hcd.symm, h₁.2.2.1, this.antisymm (dist_triangle _ _ _)⟩
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d c < dist d b + dist b c
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d c < dist d b + dist b c
⊢ False
Tactic:
replace : dist a d + dist d c + dist c a < dist a b + dist b c + dist c a := by
  linarith only [this, adb.2.2.2]
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist a d + dist d c + dist c a < dist a b + dist b c + dist c a
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist a d + dist d c + dist c a < dist a b + dist b c + dist c a
⊢ False
Tactic:
replace : ¬ NotCollinear a d c := fun h => (h₂ a d c h).not_lt this
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : ¬NotCollinear a d c
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : ¬NotCollinear a d c
⊢ False
Tactic:
simp only [notCollinear_iff, adb.ne12, hcd.symm, h₁.2.1, true_and, not_and, forall_true_left,
  ne_eq, not_forall, not_not, exists_prop, not_false_eq_true] at this
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : ∃ x, x.IsLine ∧ {a, d, c} ⊆ x
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : ∃ x, x.IsLine ∧ {a, d, c} ⊆ x
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := this
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : {a, d, c} ⊆ L
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : {a, d, c} ⊆ L
⊢ False
Tactic:
simp only [Set.subset_def, Set.mem_singleton_iff, Set.mem_insert_iff, forall_eq_or_imp,
  forall_eq] at hL'
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
⊢ False
Tactic:
have : b ∈ L := hL.close_right hL'.1 hL'.2.1 adb
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
this : b ∈ L
⊢ False

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
this : b ∈ L
⊢ False
Tactic:
refine h₁.2.2.2 L hL ?_
State after:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
this : b ∈ L
⊢ {a, b, c} ⊆ L

State before:
case 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, 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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
L : Set V
hL : L.IsLine
hL' : a ∈ L ∧ d ∈ L ∧ c ∈ L
this : b ∈ L
⊢ {a, b, c} ⊆ L
Tactic:
simp [this, hL'.1, hL'.2.2]
State after:
no goals

State before:
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
⊢ ∀ (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'
Tactic:
intro a' b' c' hL
State after:
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
a' b' c' : V
hL : NotCollinear a' b' c'
⊢ dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'

State before:
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
a' b' c' : V
hL : NotCollinear a' b' c'
⊢ dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
Tactic:
by_contra! h
State after:
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
a' b' c' : V
hL : NotCollinear a' b' c'
h : dist a' b' + dist b' c' + dist c' a' < dist a b + dist b c + dist c a
⊢ False

State before:
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
a' b' c' : V
hL : NotCollinear a' b' c'
h : dist a' b' + dist b' c' + dist c' a' < dist a b + dist b c + dist c a
⊢ False
Tactic:
exact h.ne' (h₂ a' b' c' hL h.le)
State after:
no goals

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
Tactic:
rw [not_not] at hab
State after:
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

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₁
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

State before:
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
Tactic:
exact not_not.1 <| this b c a h₁.rotate <|
  fun _ _ _ h => (h₂ _ _ _ h).trans_eq' <| by ring
State after:
no goals

State before:
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
x✝² x✝¹ x✝ : V
h : NotCollinear x✝² x✝¹ x✝
⊢ dist b c + dist c a + dist a b = dist a b + dist b c + dist c a
Tactic:
ring
State after:
no goals

State before:
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
Tactic:
exact not_not.1 <| this c a b h₁.rotate.rotate <|
  fun _ _ _ h => (h₂ _ _ _ h).trans_eq' <| by ring
State after:
no goals

State before:
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
x✝² x✝¹ x✝ : V
h : NotCollinear x✝² x✝¹ x✝
⊢ dist c a + dist a b + dist b c = dist a b + dist b c + dist c a
Tactic:
ring
State after:
no goals

State before:
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
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'
d : V
adb : sbtw a d b
hc : c ∈ Line a b
⊢ {a, b, c} ⊆ Line a b
Tactic:
simp [left_mem_Line, right_mem_Line, hc]
State after:
no goals

State before:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
⊢ dist d c < dist d b + dist b c
Tactic:
by_contra!
State after:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ False

State before:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ False
Tactic:
refine habc (generateLine_close_right hdab right_mem_Line ?_)
State after:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ sbtw d b c

State before:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ sbtw d b c
Tactic:
exact ⟨adb.ne23, hcd.symm, h₁.2.2.1, this.antisymm (dist_triangle _ _ _)⟩
State after:
no goals

State before:
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
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'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d c < dist d b + dist b c
⊢ dist a d + dist d c + dist c a < dist a b + dist b c + dist c a
Tactic:
linarith only [this, adb.2.2.2]
State after:
no goals