Theorem: two_implies_three (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, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
let S : Set (V × V × V) := setOf (fun ⟨x, y, z⟩ => SimpleTriangle x y z)
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}

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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}

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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
obtain ⟨⟨a, b, c⟩, (habc : SimpleTriangle a b c), hmin⟩ :=
  S.toFinite.exists_minimal_wrt (fun ⟨x, y, z⟩ => Delta x y z) 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, 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, a ≠ b ∧ Line a b = {a, b}

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, 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, a ≠ b ∧ Line a b = {a, b}
Tactic:
replace hmin : ∀ a' b' c' : V, SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c' := by
  intro a' b' c' h
  by_contra! h'
  exact h'.ne' (hmin (a', b', c') h 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, 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'
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}

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, 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'
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
refine ⟨a, c, habc.2.2.1.1.symm, ?_⟩
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, 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'
⊢ Line a c = {a, c}

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, 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'
⊢ Line a c = {a, c}
Tactic:
by_contra! h3
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, 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}
⊢ 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, 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}
⊢ False
Tactic:
obtain ⟨d, hd, hd'⟩ := exists_third habc.2.2.1.1.symm h3
State after:
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 d c ∨ sbtw a c d
⊢ False

State before:
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 d c ∨ sbtw a c d
⊢ False
Tactic:
simp only [habc.2.2.1.symm.2 d, false_or] at hd'
State after:
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

State before:
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
Tactic:
wlog acd : sbtw a c d generalizing a c
State after:
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

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, 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
Tactic:
clear hd'
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, 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
acd : sbtw a c d
⊢ 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, 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
acd : sbtw a c d
⊢ False
Tactic:
let S : Set V := setOf (sbtw a 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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a 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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
⊢ False
Tactic:
obtain ⟨d, hd : sbtw _ _ d, hdmin⟩ := S.toFinite.exists_minimal_wrt (dist c) S ⟨d, acd⟩
State after:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ False
Tactic:
have hbd' : b ≠ d := by
  rintro rfl
  have := habc.2.2.2.2.2.2 (Line a c) (Line_isLine hd.ne12)
  simp [right_extend_mem_Line hd] at this
State after:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
⊢ False
Tactic:
replace hdmin : ∀ d', sbtw a c d' → dist c d ≤ dist c d' := by
  intro d' hd'
  by_contra! hd''
  exact hd''.ne' (hdmin d' hd' hd''.le)
State after:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ False
Tactic:
have hcd : SimpleEdges.Adj c d := by
  use hd.2.2.1
  intro e he
  have : 0 ≤ dist e d := dist_nonneg
  have : dist e d = 0 := by linarith [he.dist, this, hdmin e (hd.right_cancel he)]
  simp only [dist_eq_zero] at this
  exact he.ne23 this
State after:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
⊢ False
Tactic:
have hbd := eqn_7 habc hmin hd hcd
State after:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
⊢ False
Tactic:
let S : Set (List V) := setOf (List.Special a b d)
State after:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
⊢ False
Tactic:
have : S.Finite := by
  have ⟨n, hn⟩ := uniformly_bounded_of_chain_ne_of_pathLength_le V [a, b, d].pathLength
  exact (List.finite_length_le _ _).subset fun l hl => hn l hl.chain_ne hl.pathLength_le
State after:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
⊢ False
Tactic:
have ⟨P, (hP : P.Special a b d), hPmin⟩ :=
  this.exists_minimal_wrt List.pathLength S ⟨[a, b, d], abd_special habc hd hbd' hbd⟩
State after:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ False

State before:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ False
Tactic:
replace hPmin : ∀ P' : List V, P'.Special a b d → P.pathLength ≤ P'.pathLength := by
  intro P' hP'
  by_contra! h
  exact h.ne' (hPmin P' hP' h.le)
State after:
case 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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ 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, 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'
Tactic:
intro a' b' c' 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, 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'

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, 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'
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, 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'
h' : Delta a' b' c' < Delta a b 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, 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'
h' : Delta a' b' c' < Delta a b c
⊢ False
Tactic:
exact h'.ne' (hmin (a', b', c') h h'.le)
State after:
no goals

State before:
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
Tactic:
rw [Line_comm] at hd h3
State after:
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 c a ≠ {a, c}
d : V
hd : d ∈ Line c a
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

State before:
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 c a ≠ {a, c}
d : V
hd : d ∈ Line c a
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
Tactic:
rw [Set.pair_comm] at h3
State after:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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

State before:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
Tactic:
have h' := hd'.resolve_right acd
State after:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h' : sbtw d a c
⊢ False

State before:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h' : sbtw d a c
⊢ False
Tactic:
refine this c a habc.swap ?_ h3 hd (Or.inr h'.symm) h'.symm
State after:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h' : sbtw d a c
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta c b a ≤ Delta a' b' c'

State before:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h' : sbtw d a c
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta c b a ≤ Delta a' b' c'
Tactic:
intro a' b' c' h'
State after:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta c b a ≤ Delta a' b' c'

State before:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta c b a ≤ Delta a' b' c'
Tactic:
rw [Delta_comm]
State after:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'

State before:
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 c a ≠ {c, a}
d : V
hd : d ∈ Line c a
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'
Tactic:
exact hmin _ _ _ h'
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ b ≠ d
Tactic:
rintro rfl
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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = 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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
⊢ False
Tactic:
have := habc.2.2.2.2.2.2 (Line a c) (Line_isLine hd.ne12)
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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
this : ¬{a, b, c} ⊆ Line a 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, 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
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
this : ¬{a, b, c} ⊆ Line a c
⊢ False
Tactic:
simp [right_extend_mem_Line hd] at this
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
⊢ ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
Tactic:
intro d' hd'
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
d' : V
hd' : sbtw a c d'
⊢ dist c d ≤ dist c d'

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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
d' : V
hd' : sbtw a c d'
⊢ dist c d ≤ dist c d'
Tactic:
by_contra! hd''
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
d' : V
hd' : sbtw a c d'
hd'' : dist c d' < dist c d
⊢ 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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
d' : V
hd' : sbtw a c d'
hd'' : dist c d' < dist c d
⊢ False
Tactic:
exact hd''.ne' (hdmin d' hd' hd''.le)
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ SimpleEdges.Adj c d
Tactic:
use hd.2.2.1
State after:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ ∀ (x : V), ¬sbtw c x d

State before:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ ∀ (x : V), ¬sbtw c x d
Tactic:
intro e he
State after:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
⊢ False

State before:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
⊢ False
Tactic:
have : 0 ≤ dist e d := dist_nonneg
State after:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ False

State before:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ False
Tactic:
have : dist e d = 0 := by linarith [he.dist, this, hdmin e (hd.right_cancel he)]
State after:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : dist e d = 0
⊢ False

State before:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : dist e d = 0
⊢ False
Tactic:
simp only [dist_eq_zero] at this
State after:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : e = d
⊢ False

State before:
case right
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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : e = d
⊢ False
Tactic:
exact he.ne23 this
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, 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
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ dist e d = 0
Tactic:
linarith [he.dist, this, hdmin e (hd.right_cancel he)]
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
⊢ S.Finite
Tactic:
have ⟨n, hn⟩ := uniformly_bounded_of_chain_ne_of_pathLength_le V [a, b, d].pathLength
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
n : ℕ
hn : ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ [a, b, d].pathLength → l.length ≤ n
⊢ S.Finite

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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
n : ℕ
hn : ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ [a, b, d].pathLength → l.length ≤ n
⊢ S.Finite
Tactic:
exact (List.finite_length_le _ _).subset fun l hl => hn l hl.chain_ne hl.pathLength_le
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
Tactic:
intro P' hP'
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
⊢ P.pathLength ≤ P'.pathLength

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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
⊢ P.pathLength ≤ P'.pathLength
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
h : P'.pathLength < P.pathLength
⊢ 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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
h : P'.pathLength < P.pathLength
⊢ False
Tactic:
exact h.ne' (hPmin P' hP' h.le)
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hP : List.Special a b d (a₁ :: a₂ :: a₃ :: l)
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
⊢ False
Tactic:
simp only [List.Special] at hP
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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hP :
  a₁ = a ∧
    NotCollinear a₁ a₂ a₃ ∧
      (¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃) ∧
        (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d ∧
          List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l) ∧
            (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
⊢ 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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hP :
  a₁ = a ∧
    NotCollinear a₁ a₂ a₃ ∧
      (¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃) ∧
        (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d ∧
          List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l) ∧
            (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
⊢ False
Tactic:
rcases hP with ⟨ha₁, hα, hβ, hPd, hPc, _⟩
State after:
case intro.intro.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ False

State before:
case intro.intro.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ False
Tactic:
have : (¬ SimpleEdges.Adj a₁ a₂ ∧ ¬ SimpleEdges.Adj a₂ a₃) ∨
      (SimpleEdges.Adj a₁ a₂ ∧ ¬ SimpleEdges.Adj a₂ a₃) ∨
      (¬ SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃) := by tauto
State after:
case intro.intro.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this✝ : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
this :
  ¬SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨
    SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨ ¬SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃
⊢ False

State before:
case intro.intro.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this✝ : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
this :
  ¬SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨
    SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨ ¬SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
rcases this with (⟨c₁1, c₁2⟩ | ⟨c₂1, c₂2⟩ | ⟨c₃1, c₃2⟩)
State after:
case intro.intro.intro.intro.intro.inl.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False

case intro.intro.intro.intro.intro.inr.inl.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₂1 : SimpleEdges.Adj a₁ a₂
c₂2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False

case intro.intro.intro.intro.intro.inr.inr.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₃1 : ¬SimpleEdges.Adj a₁ a₂
c₃2 : SimpleEdges.Adj a₂ 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, 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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ ¬SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨
    SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨ ¬SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃
Tactic:
tauto
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case1 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₁1 c₁2
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inl.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₂1 : SimpleEdges.Adj a₁ a₂
c₂2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case2 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₂1 c₂2
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inr.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
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
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₃1 : ¬SimpleEdges.Adj a₁ a₂
c₃2 : SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case3 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₃1 c₃2
State after:
no goals