internlm/Lean-Github huggingface dataset:
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b = m ∨ b ∉ t
⊢ b < a
Tactic:
obtain rfl | hbt := hbt
Proof state after:
case inr.intro.intro.intro.inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
hbs : m ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
⊢ m < a

case inr.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
⊢ b < a
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
hbs : m ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
⊢ m < a
Tactic:
assumption
Proof state after:
no goals
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
⊢ b < a
Tactic:
by_contra! hab
Proof state after:
case inr.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
hab : a ≤ b
⊢ False
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
hab : a ≤ b
⊢ False
Tactic:
exact hbt $ (hw $ hwa.trans_le hab).1 $ mem_of_mem_erase hbs
Proof state after:
no goals
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
have : erase t m ⊆ erase s a := by
  rintro b hb
  rw [mem_erase] at hb ⊢
  exact ⟨(haw.trans_le $ min'_le _ _ hb.2).ne', (hw $ hb.1.lt_of_le' $ min'_le _ _ hb.2).2 hb.2⟩
Proof state after:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
rw [eq_of_subset_of_card_le this]
Proof state after:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ (s.erase a).card ≤ (t.erase m).card
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ (s.erase a).card ≤ (t.erase m).card
Tactic:
rw [card_erase_of_mem ha, card_erase_of_mem (min'_mem _ _)]
Proof state after:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ s.card - 1 ≤ t.card - 1
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ s.card - 1 ≤ t.card - 1
Tactic:
exact tsub_le_tsub_right hcard _
Proof state after:
no goals
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
⊢ t.erase m ⊆ s.erase a
Tactic:
rintro b hb
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
b : α
hb : b ∈ t.erase m
⊢ b ∈ s.erase a
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
b : α
hb : b ∈ t.erase m
⊢ b ∈ s.erase a
Tactic:
rw [mem_erase] at hb ⊢
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
b : α
hb : b ≠ m ∧ b ∈ t
⊢ b ≠ a ∧ b ∈ s
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
b : α
hb : b ≠ m ∧ b ∈ t
⊢ b ≠ a ∧ b ∈ s
Tactic:
exact ⟨(haw.trans_le $ min'_le _ _ hb.2).ne', (hw $ hb.1.lt_of_le' $ min'_le _ _ hb.2).2 hb.2⟩
Proof state after:
no goals
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
refine (lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws,
  fun b hbs hbt ↦ ?_⟩).le
Proof state after:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ { ofColex := { val := t.val.erase m, nodup := ⋯ } }.ofColex
⊢ b < w
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ { ofColex := { val := t.val.erase m, nodup := ⋯ } }.ofColex
⊢ b < w
Tactic:
change b ∉ t.erase m at hbt
Proof state after:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t.erase m
⊢ b < w
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t.erase m
⊢ b < w
Tactic:
rw [mem_erase, not_and_or, not_ne_iff] at hbt
Proof state after:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b = m ∨ b ∉ t
⊢ b < w
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b = m ∨ b ∉ t
⊢ b < w
Tactic:
obtain rfl | hbt := hbt
Proof state after:
case inr.intro.intro.intro.inr.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
hbs : m ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
⊢ m < w

case inr.intro.intro.intro.inr.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
⊢ b < w
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
hbs : m ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
⊢ m < w
Tactic:
assumption
Proof state after:
no goals
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
⊢ b < w
Tactic:
by_contra! hwb
Proof state after:
case inr.intro.intro.intro.inr.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
hwb : w ≤ b
⊢ False
Theorem: Finset.Colex.erase_le_erase_min'
Proof state before:
case inr.intro.intro.intro.inr.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ t
hwb : w ≤ b
⊢ False
Tactic:
exact hbt $ (hw $ hwb.lt_of_ne $ ne_of_mem_of_not_mem hwt hbt).1 $ mem_of_mem_erase hbs
Proof state after:
no goals
Theorem: generateLine_minimal
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
⊢ GenerateLine S ⊆ L
Tactic:
intro x hx
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x : V
hx : x ∈ GenerateLine S
⊢ x ∈ L
Theorem: generateLine_minimal
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x : V
hx : x ∈ GenerateLine S
⊢ x ∈ L
Tactic:
induction hx with
| basic h => exact hL₀ h
| extend_out u v w _ _ hw hu hv => exact out_closed hu hv hw
| extend_in u v w _ _ hw hu hv => exact in_closed hu hv hw
Proof state after:
no goals
Theorem: generateLine_minimal
Proof state before:
case basic
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x x✝ : V
h : x✝ ∈ S
⊢ x✝ ∈ L
Tactic:
exact hL₀ h
Proof state after:
no goals
Theorem: generateLine_minimal
Proof state before:
case extend_out
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x u v w : V
a✝¹ : GenerateLine S u
a✝ : GenerateLine S v
hw : sbtw u v w
hu : u ∈ L
hv : v ∈ L
⊢ w ∈ L
Tactic:
exact out_closed hu hv hw
Proof state after:
no goals
Theorem: generateLine_minimal
Proof state before:
case extend_in
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x u v w : V
a✝¹ : GenerateLine S u
a✝ : GenerateLine S v
hw : sbtw u w v
hu : u ∈ L
hv : v ∈ L
⊢ w ∈ L
Tactic:
exact in_closed hu hv hw
Proof state after:
no goals
Theorem: left_mem_Line
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w a b : V
⊢ a ∈ {a, b}
Tactic:
simp
Proof state after:
no goals
Theorem: right_mem_Line
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w a b : V
⊢ b ∈ {a, b}
Tactic:
simp
Proof state after:
no goals
Theorem: Line_comm
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
⊢ Line u v = Line v u
Tactic:
rw [Line, Line, Set.pair_comm]
Proof state after:
no goals
Theorem: Set.IsLine.close_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
L : Set V
hL : L.IsLine
a b c : V
ha : a ∈ L
hb : b ∈ L
hc : sbtw a b c
⊢ c ∈ L
Tactic:
obtain ⟨x, y, _, rfl⟩ := hL
Proof state after:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw a b c
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Theorem: Set.IsLine.close_right
Proof state before:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw a b c
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Tactic:
exact generateLine_close_right ha hb hc
Proof state after:
no goals
Theorem: Set.IsLine.close_left
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
L : Set V
hL : L.IsLine
a b c : V
ha : a ∈ L
hb : b ∈ L
hc : sbtw c a b
⊢ c ∈ L
Tactic:
obtain ⟨x, y, _, rfl⟩ := hL
Proof state after:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw c a b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Theorem: Set.IsLine.close_left
Proof state before:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw c a b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Tactic:
exact generateLine_close_left ha hb hc
Proof state after:
no goals
Theorem: Set.IsLine.close_middle
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
L : Set V
hL : L.IsLine
a b c : V
ha : a ∈ L
hb : b ∈ L
hc : sbtw a c b
⊢ c ∈ L
Tactic:
obtain ⟨x, y, _, rfl⟩ := hL
Proof state after:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw a c b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Theorem: Set.IsLine.close_middle
Proof state before:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw a c b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Tactic:
exact generateLine_close_middle ha hb hc
Proof state after:
no goals
Theorem: exists_isLine
Proof 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
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L
Tactic:
rcases ne_or_eq a b with h | rfl
Proof state after:
case inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : a ≠ b
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L

case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Theorem: exists_isLine
Proof state before:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Tactic:
have ⟨b, h⟩ := exists_ne a
Proof state after:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : b ≠ a
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Theorem: exists_isLine
Proof state before:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : b ≠ a
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Tactic:
exact ⟨Line a b, Line_isLine h.symm, by simp⟩
Proof state after:
no goals
Theorem: exists_isLine
Proof state before:
case inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : a ≠ b
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L
Tactic:
exact ⟨Line a b, Line_isLine h, by simp⟩
Proof state after:
no goals
Theorem: exists_isLine
Proof 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
h : a ≠ b
⊢ {a, b} ⊆ Line a b
Tactic:
simp
Proof state after:
no goals
Theorem: exists_isLine
Proof 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
h : b ≠ a
⊢ {a, a} ⊆ Line a b
Tactic:
simp
Proof state after:
no goals
Theorem: NotCollinear.mk
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ NotCollinear x y z
Tactic:
refine ⟨?_, ?_, ?_, hl⟩
Proof 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 : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ y

case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ z

case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ y ≠ z
Theorem: NotCollinear.mk
Proof 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 : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ y
Tactic:
rintro rfl
Proof state after:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
⊢ False
Theorem: NotCollinear.mk
Proof state before:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x z
Proof state after:
case refine_1.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, z} ⊆ L
⊢ False
Theorem: NotCollinear.mk
Proof state before:
case refine_1.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, z} ⊆ L
⊢ False
Tactic:
aesop
Proof state after:
no goals
Theorem: NotCollinear.mk
Proof 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 : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ z
Tactic:
rintro rfl
Proof state after:
case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
⊢ False
Theorem: NotCollinear.mk
Proof state before:
case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x y
Proof state after:
case refine_2.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False
Theorem: NotCollinear.mk
Proof state before:
case refine_2.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False
Tactic:
aesop
Proof state after:
no goals
Theorem: NotCollinear.mk
Proof state before:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ y ≠ z
Tactic:
rintro rfl
Proof state after:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
⊢ False
Theorem: NotCollinear.mk
Proof state before:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x y
Proof state after:
case refine_3.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False