-- Mathlib/Combinatorics/Colex.lean
/-- If `s ≤ t` in colex and `#s ≤ #t`, then `s \ {a} ≤ t \ {min t}` for any `a ∈ s`. -/
lemma erase_le_erase_min' (hst : toColex s ≤ toColex t) (hcard : #s ≤ #t) (ha : a ∈ s) :
    toColex (s.erase a) ≤
      toColex (t.erase <| min' t <| card_pos.1 <| (card_pos.2 ⟨a, ha⟩).trans_le hcard)

Proof state:
case inr.intro.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
case inr.intro.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Proof state:
case inr.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 }

Proof state:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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]

Result:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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) ≤ #(t.erase m)

Proof state:
case inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 }

Proof state:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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) ≤ #(t.erase m)

Tactic:
rw [card_erase_of_mem ha, card_erase_of_mem (min'_mem _ _)]

Result:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 - 1 ≤ #t - 1

Proof state:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 - 1 ≤ #t - 1

Tactic:
exact tsub_le_tsub_right hcard _

Result:
no goals

Proof state:
case inr.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
case inr.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 }

Proof state:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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⟩

Result:
case inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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 }

Proof state:
case inr.intro.intro.intro.inl.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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

Result:
case inr.intro.intro.intro.inl.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
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