Theorem: thm_two (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 : V), ¬NotCollinear x y z
⊢ Set.univ.IsLine
Tactic:
let S : Set (Set V) := setOf Set.IsLine
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
⊢ Set.univ.IsLine

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
⊢ Set.univ.IsLine
Tactic:
have : S.Nonempty := let ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨_, Line_isLine hxy⟩
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
⊢ Set.univ.IsLine

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
⊢ Set.univ.IsLine
Tactic:
obtain ⟨L, hL, hL'⟩ := S.toFinite.exists_maximal_wrt id S 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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, id L ≤ id a' → id L = id a'
⊢ Set.univ.IsLine

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, id L ≤ id a' → id L = id a'
⊢ Set.univ.IsLine
Tactic:
dsimp at hL'
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ Set.univ.IsLine

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ Set.univ.IsLine
Tactic:
suffices L = Set.univ by rwa [← 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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ L = Set.univ

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ L = Set.univ
Tactic:
rw [Set.eq_univ_iff_forall]
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ ∀ (x : V), x ∈ L

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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ ∀ (x : V), x ∈ L
Tactic:
by_contra!
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : ∃ x, x ∉ L
⊢ 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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : ∃ x, x ∉ L
⊢ False
Tactic:
obtain ⟨a, b, hab, rfl⟩ := hL
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
this : ∃ x, x ∉ Line a b
⊢ 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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
this : ∃ x, x ∉ Line a b
⊢ False
Tactic:
obtain ⟨c, hc'⟩ := this
State after:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
⊢ False

State before:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
⊢ False
Tactic:
have hac : a ≠ c := fun h => hc' (subset_generateLine _ (by simp [h]))
State after:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
⊢ False

State before:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
⊢ False
Tactic:
have hbc : b ≠ c := fun h => hc' (subset_generateLine _ (by simp [h]))
State after:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
⊢ False

State before:
case intro.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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Tactic:
simp only [NotCollinear, not_and, not_forall, not_not] at h
State after:
case intro.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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
⊢ False

State before:
case intro.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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
⊢ False
Tactic:
obtain ⟨M, hM, habc⟩ := h a b c hab hac hbc
State after:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ False

State before:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ False
Tactic:
have := hL' M hM (Set.IsLine.generateLine_subset (habc.trans' (by simp)) hM)
State after:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False

State before:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Tactic:
rw [this] at hc'
State after:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False

State before:
case intro.intro.intro.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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Tactic:
exact hc' (habc (by simp))
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : L = Set.univ
⊢ Set.univ.IsLine
Tactic:
rwa [← 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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
h : a = c
⊢ c ∈ {a, b}
Tactic:
simp [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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
h : b = c
⊢ c ∈ {a, b}
Tactic:
simp [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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ {a, b} ≤ {a, b, c}
Tactic:
simp
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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ c ∈ {a, b, c}
Tactic:
simp
State after:
no goals