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

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase (t.min' ⋯) }
Tactic:
generalize_proofs ht
State after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase (t.min' ht) }

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase (t.min' ht) }
Tactic:
set m := min' t ht
State after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
obtain rfl | h' := eq_or_ne s t
State after:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst : { ofColex := s } ≤ { ofColex := s }
hcard : s.card ≤ s.card
ht : s.Nonempty
m : α := s.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase m }

case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
replace hst := hst.lt_of_ne $ toColex_inj.not.2 h'
State after:
case 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
hst : { ofColex := s } < { ofColex := t }
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
case 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
hst : { ofColex := s } < { ofColex := t }
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
simp only [lt_iff_exists_forall_lt_mem_iff_mem] at hst
State after:
case 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
hst : ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
case 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
hst : ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
obtain ⟨w, hwt, hws, hw⟩ := hst
State after:
case inr.intro.intro.intro
α : 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)
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
case inr.intro.intro.intro
α : 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)
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_lt
State after:
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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

case inr.intro.intro.intro.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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

State before:
case inr.intro.intro.intro.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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt
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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

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 }

State before:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst : { ofColex := s } ≤ { ofColex := s }
hcard : s.card ≤ s.card
ht : s.Nonempty
m : α := s.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase m }
Tactic:
exact (erase_le_erase ha $ min'_mem _ _).2 $ min'_le _ _ $ ha
State after:
no goals

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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
have hma : m < a := (min'_le _ _ hwt).trans_lt hwa
State after:
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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

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
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
Tactic:
refine (lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
  not_mem_erase _ _, fun b hbs hbt ↦ ?_⟩).le
State after:
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 ∉ { ofColex := { val := t.val.erase m, nodup := ⋯ } }.ofColex
⊢ b < a

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 ∉ { ofColex := { val := t.val.erase m, nodup := ⋯ } }.ofColex
⊢ b < a
Tactic:
change b ∉ t.erase m at hbt
State after:
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 ∉ t.erase m
⊢ b < a

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 ∉ t.erase m
⊢ b < a
Tactic:
rw [mem_erase, not_and_or, not_ne_iff] at hbt
State after:
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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⟩
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 }

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]
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

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 _ _)]
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

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 _
State after:
no goals

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
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

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 ⊢
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

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⟩
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals