Theorem: exists_third (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
h : Line a b ≠ {a, b}
⊢ ∃ c ∈ Line a b, sbtw c a b ∨ sbtw a c b ∨ sbtw 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
this : Line a b = {a, b}
⊢ False
Tactic:
exact h 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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b = {a, b}
Tactic:
refine (subset_generateLine _).antisymm' ?_
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ GenerateLine {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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ GenerateLine {a, b} ⊆ {a, b}
Tactic:
change Line a b ⊆ {a, b}
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b ⊆ {a, b}
Tactic:
refine generateLine_minimal le_rfl ?_ ?_
State after:
case refine_1
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x y z → z ∈ {a, b}

case refine_2
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x z y → z ∈ {a, b}

State before:
case refine_1
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x y z → z ∈ {a, b}
Tactic:
rintro x y z (rfl | rfl) (rfl | rfl) h
State after:
case refine_1.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y y z
⊢ z ∈ {y, b}

case refine_1.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x y z
⊢ z ∈ {x, y}

case refine_1.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x y z
⊢ z ∈ {y, x}

case refine_1.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y y z
⊢ z ∈ {a, y}

State before:
case refine_1.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y y z
⊢ z ∈ {y, b}
Tactic:
exact (h.ne12 rfl).elim
State after:
no goals

State before:
case refine_1.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x y z
⊢ z ∈ {x, y}
Tactic:
exact ((h' z (right_extend_mem_Line h)).2.2 h).elim
State after:
no goals

State before:
case refine_1.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x y z
⊢ z ∈ {y, x}
Tactic:
exact ((h' z (left_extend_mem_Line h.symm)).1 h.symm).elim
State after:
no goals

State before:
case refine_1.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y y z
⊢ z ∈ {a, y}
Tactic:
exact (h.ne12 rfl).elim
State after:
no goals

State before:
case refine_2
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
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x z y → z ∈ {a, b}
Tactic:
rintro x y z (rfl | rfl) (rfl | rfl) h
State after:
case refine_2.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y z y
⊢ z ∈ {y, b}

case refine_2.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x z y
⊢ z ∈ {x, y}

case refine_2.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x z y
⊢ z ∈ {y, x}

case refine_2.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y z y
⊢ z ∈ {a, y}

State before:
case refine_2.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y z y
⊢ z ∈ {y, b}
Tactic:
exact (h.ne13 rfl).elim
State after:
no goals

State before:
case refine_2.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x z y
⊢ z ∈ {x, y}
Tactic:
exact ((h' z (middle_extend_mem_Line h)).2.1 h).elim
State after:
no goals

State before:
case refine_2.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x z y
⊢ z ∈ {y, x}
Tactic:
exact ((h' z (middle_extend_mem_Line h.symm)).2.1 h.symm).elim
State after:
no goals

State before:
case refine_2.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y z y
⊢ z ∈ {a, y}
Tactic:
exact (h.ne13 rfl).elim
State after:
no goals