Theorem: Finset.Colex.lt_iff_exists_forall_lt_mem_iff_mem (LeanCamCombi/Mathlib/Combinatorics/Colex.lean)

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ { ofColex := s } < { ofColex := t } ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
simp only [lt_iff_exists_forall_lt]
State after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

case refine_2
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) → ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
let u := (t \ s).filter fun w ↦ ∀ a ∈ s, a ∉ t → a < w
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [u, and_assoc]
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
let m := max' _ hu
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 $ max'_mem _ _
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic:
refine ⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
⊢ a ∈ s

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
⊢ a ∈ s
Tactic:
by_contra has
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
⊢ False

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
⊢ False
Tactic:
have hau : a ∈ u := mem_u.2 ⟨hat, has, fun b hbs hbt ↦ (hm _ hbs hbt).trans hma⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
hau : a ∈ u
⊢ False

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
hau : a ∈ u
⊢ False
Tactic:
exact hma.not_le $ le_max' _ _ hau
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
w : α
⊢ w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
Tactic:
simp [u, and_assoc]
State after:
no goals

State before:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) → ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Tactic:
rintro ⟨w, hwt, hws, hw⟩
State after:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

State before:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Tactic:
refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩
State after:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
⊢ a < w

State before:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
⊢ a < w
Tactic:
by_contra! hwa
State after:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
hwa : w ≤ a
⊢ False

State before:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
hwa : w ≤ a
⊢ False
Tactic:
exact hat $ (hw $ hwa.lt_of_ne $ ne_of_mem_of_not_mem hwt hat).1 has
State after:
no goals