Theorem: sylvester_chvatal (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✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
by_cases h : ∀ x y z : V, ¬ NotCollinear x y z
State after:
case pos
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ¬∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

State before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ¬∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
push_neg at h
State after:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

State before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
replace h := one_implies_two h
State after:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

State before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
obtain ⟨a, b, h, hl⟩ := two_implies_three h
State after:
case neg.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h✝ : ∃ x y z, SimpleTriangle x y z
a b : V
h : a ≠ b
hl : Line a b = {a, b}
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

State before:
case neg.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h✝ : ∃ x y z, SimpleTriangle x y z
a b : V
h : a ≠ b
hl : Line a b = {a, b}
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
exact ⟨a, b, h, Or.inl hl⟩
State after:
no goals

State before:
case pos
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
obtain ⟨L, hL, a, b, hab, rfl⟩ := thm_two' h
State after:
case pos.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✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
a b : V
hab : a ≠ b
hL : Line a b = Set.univ
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

State before:
case pos.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✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
a b : V
hab : a ≠ b
hL : Line a b = Set.univ
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
exact ⟨a, b, hab, Or.inr hL⟩
State after:
no goals