Theorem: exists_simple_split_right (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 a b : V
hab : a ≠ b
hab' : ¬SimpleEdges.Adj a b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
simp only [SimpleEdges_adj, hab, not_false_eq_true, true_and, ne_eq, 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 a b : V
hab : a ≠ b
hab' : ∃ x, sbtw a x b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
hab' : ∃ x, sbtw a x b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
obtain ⟨c', hc'⟩ := 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 a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b

State before:
case intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
obtain ⟨c, hc : sbtw _ c _, hcmin⟩ := S.toFinite.exists_minimal_wrt (dist b) _ ⟨c', hc'⟩
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 a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b

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 a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
refine ⟨c, hc, hc.ne23, fun c' hc' => ?_⟩
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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
⊢ 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
⊢ False
Tactic:
have : dist b c ≤ dist b c' :=
  le_of_not_lt fun h => h.ne' <| hcmin _ (hc.trans_right' hc') h.le
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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist b c ≤ dist b c'
⊢ 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist b c ≤ dist b c'
⊢ False
Tactic:
rw [dist_comm b, dist_comm b] at 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ False
Tactic:
have : dist c c' ≤ 0 := by linarith [hc'.dist]
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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : dist c c' ≤ 0
⊢ 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : dist c c' ≤ 0
⊢ False
Tactic:
simp only [dist_le_zero] at 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : c = c'
⊢ 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : c = c'
⊢ False
Tactic:
exact hc'.ne12 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 a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ dist c c' ≤ 0
Tactic:
linarith [hc'.dist]
State after:
no goals