awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
inl :
  ∀
    (hst :
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)))
    (hcard : #s ≤ #s) (ht : s.Nonempty),
    let m := s.min' ht;
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase m) : Colex (Finset α))
inr :
  ∀ (h' : s ≠ t),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
obtain rfl | h' := eq_or_ne s t

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
hcard : #s ≤ #s
ht : s.Nonempty
m : α := s.min' ht
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase m) : Colex (Finset α))

Tactic:
(erase_le_erase ha <| min'_mem _ _).2 <| min'_le _ _ <| ha

Premises used: Iff.mpr, Finset.min'_le, Set.Mem, Finset.Colex.erase_le_erase, setOf, Finset.min'_mem
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
hcard : #s ≤ #s
ht : s.Nonempty
m : α := s.min' ht
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase m) : Colex (Finset α))

Tactic:
exact (erase_le_erase ha <| min'_mem _ _).2 <| min'_le _ _ <| ha

Premises used: Iff.mpr, Finset.min'_le, Finset.Colex.erase_le_erase, Finset.min'_mem
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
replace hst := hst.lt_of_ne <| toColex_inj.not.2 h'
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
simp only [lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc] at hst

Premises used: Finset.Colex.lt_iff_exists_filter_lt, Finset.mem_sdiff, and_assoc, Finset.filter_inj
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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)
inr :
  ∀ (w : α) (hwt : w ∈ t) (hws : w ∉ s) (hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
obtain ⟨w, hwt, hws, hw⟩ := hst
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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)
inr :
  ∀ (hwa : w < a),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
inr₁ :
  ∀ (haw : a < w),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_gt

Premises used: Ne.symm, ne_of_mem_of_not_mem, Ne.lt_or_gt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
⊢ m < a

Tactic:
have hma : m < a := (min'_le _ _ hwt).trans_lt hwa
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
(lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
      notMem_erase _ _, fun b hbs hbt ↦ ?_⟩).le

Premises used: Iff.mpr, Finset.Colex.lt_iff_exists_forall_lt, Set.Mem, setOf, LT.lt.le, LT.lt.ne', Finset.mem_erase, And.intro, Exists.intro, Iff.mp, Finset.notMem_erase
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
inr :
  ∀ (b : α)
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b)
    (hbt :
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)),
    b < a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
refine (lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
      notMem_erase _ _, fun b hbs hbt ↦ ?_⟩).le

Premises used: Iff.mpr, Finset.Colex.lt_iff_exists_forall_lt, LT.lt.le, LT.lt.ne', Finset.mem_erase, And.intro, Exists.intro, Iff.mp, Finset.notMem_erase
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)
⊢ b ∉ t.erase m

Tactic:
change b ∉ t.erase m at hbt

Premises used: Finset.erase
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t.erase m
⊢ b = m ∨ b ∉ t

Tactic:
rw [mem_erase, not_and_or, not_ne_iff] at hbt

Premises used: not_ne_iff, Finset.mem_erase, not_and_or
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
inr :
  ∀
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m),
    m < a
inr₁ : ∀ (hbt : b ∉ t), b < a
⊢ b < a

Tactic:
obtain rfl | hbt := hbt

Premises used: rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m
⊢ m < a

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
inr : ∀ (hab : a ≤ b), False
⊢ b < a

Tactic:
by_contra! hab
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
hab : a ≤ b
⊢ False

Tactic:
hbt <| (hw <| hwa.trans_le hab).1 <| mem_of_mem_erase hbs

Premises used: LT.lt.trans_le, Finset.mem_of_mem_erase, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
hab : a ≤ b
⊢ False

Tactic:
exact hbt <| (hw <| hwa.trans_le hab).1 <| mem_of_mem_erase hbs

Premises used: LT.lt.trans_le, Finset.mem_of_mem_erase, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
⊢ m = w ∨ m < w

Tactic:
(min'_le _ _ hwt).eq_or_lt

Premises used: LE.le.eq_or_lt, Finset.min'_le
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
inr :
  ∀ (hwt : m ∈ t) (hws : m ∉ s) (hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)) (haw : a < m),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
inr₁ :
  ∀ (hmw : m < w),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt

Premises used: LE.le.eq_or_lt, Finset.min'_le, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 ∈ t.erase m
rw : ∀ (hb : b ≠ m ∧ b ∈ t), b ≠ a ∧ b ∈ s
⊢ b ∈ s.erase a

Tactic:
rw [mem_erase] at hb ⊢

Premises used: Finset.mem_erase
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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:
⟨(haw.trans_le <| min'_le _ _ hb.2).ne',
        (hw <| hb.1.lt_of_le' <| min'_le _ _ hb.2).2 hb.2⟩

Premises used: Iff.mpr, Finset.min'_le, LT.lt.ne', And.right, And.left, LT.lt.trans_le, And.intro, Ne.lt_of_le'
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
⊢ t.erase m ⊆ s.erase a

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⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
inr : #(s.erase a) ≤ #(t.erase m)
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
rw [eq_of_subset_of_card_le this]

Premises used: Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
inr : #s - 1 ≤ #t - 1
⊢ #(s.erase a) ≤ #(t.erase m)

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

Premises used: Finset.min'_mem, Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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:
tsub_le_tsub_right hcard _

Premises used: tsub_le_tsub_right
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 _

Premises used: tsub_le_tsub_right
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

Tactic:
(lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws,
      fun b hbs hbt ↦ ?_⟩).le

Premises used: Iff.mpr, Finset.Colex.lt_iff_exists_forall_lt, Set.Mem, setOf, mt, LT.lt.le, LT.lt.ne', Finset.mem_erase, Finset.mem_of_mem_erase, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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
inr :
  ∀ (b : α)
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b)
    (hbt :
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)),
    b < w
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))

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

Premises used: Iff.mpr, Finset.Colex.lt_iff_exists_forall_lt, mt, LT.lt.le, LT.lt.ne', Finset.mem_erase, Finset.mem_of_mem_erase, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)
⊢ b ∉ t.erase m

Tactic:
change b ∉ t.erase m at hbt

Premises used: Finset.erase
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t.erase m
⊢ b = m ∨ b ∉ t

Tactic:
rw [mem_erase, not_and_or, not_ne_iff] at hbt

Premises used: not_ne_iff, Finset.mem_erase, not_and_or
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
inr :
  ∀
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m),
    m < w
inr₁ : ∀ (hbt : b ∉ t), b < w
⊢ b < w

Tactic:
obtain rfl | hbt := hbt

Premises used: rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m
⊢ m < w

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
inr : ∀ (hwb : w ≤ b), False
⊢ b < w

Tactic:
by_contra! hwb
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
hwb : w ≤ b
⊢ False

Tactic:
hbt <| (hw <| hwb.lt_of_ne <| ne_of_mem_of_not_mem hwt hbt).1 <| mem_of_mem_erase hbs

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, Finset.mem_of_mem_erase, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : 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 :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
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

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, Finset.mem_of_mem_erase, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s t : Finset α
hf : StrictMono f
⊢ LE.le (α := Colex (Finset β)) ((toColex : (a : Finset β) → Colex (Finset β)) (image f s) : Colex (Finset β))
      ((toColex : (a : Finset β) → Colex (Finset β)) (image f t) : Colex (Finset β)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff]

Premises used: Function.Injective.eq_iff, Finset.Colex.toColex_le_toColex, StrictMono.injective, StrictMono.le_iff_le
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s t : Finset α
hf : StrictMono f
⊢ LT.lt (α := Colex (Finset β)) ((toColex : (a : Finset β) → Colex (Finset β)) (image f s) : Colex (Finset β))
      ((toColex : (a : Finset β) → Colex (Finset β)) (image f t) : Colex (Finset β)) ↔
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
lt_iff_lt_of_le_iff_le <| toColex_image_le_toColex_image hf

Premises used: Finset.Colex.toColex_image_le_toColex_image, lt_iff_lt_of_le_iff_le