Theorem: two_implies_three
Proof 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⟩)
Proof 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