awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
refine_1 :
  ∀
    (h :
      ∃ (a : α),
        Membership.mem (γ := Finset α)
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
              Finset α)
            a ∧
          a ∉
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α) ∧
            ∀ (b : α),
              Membership.mem (γ := Finset α)
                  ((ofColex : (a : Colex (Finset α)) → Finset α)
                      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                    Finset α)
                  b →
                b ∉
                    ((ofColex : (a : Colex (Finset α)) → Finset α)
                        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                      Finset α) →
                  b < a),
    ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ (∃ (a : α),
      Membership.mem (γ := Finset α)
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
            Finset α)
          a ∧
        a ∉
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
              Finset α) ∧
          ∀ (b : α),
            Membership.mem (γ := Finset α)
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                  Finset α)
                b →
              b ∉
                  ((ofColex : (a : Colex (Finset α)) → Finset α)
                      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                    Finset α) →
                b < a) ↔
    ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
have refine_2 : (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) →
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
have mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
Tactic: have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [u, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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)
have hu : u.Nonempty
Tactic: have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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)
have hmt : m ∈ t
Tactic: have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
have hms : m ∉ s
Tactic: have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
have hm : ∀ a ∈ s, a ∉ t → a < m
Tactic: have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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)
have refine_1 : ∀ (a : α) (hma : m < a) (hat : a ∈ t), a ∈ s
Tactic: refine ⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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
have refine_1 : ∀ (has : a ∉ s), False
Tactic: by_contra has
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
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
have hau : a ∈ u
Tactic: have hau : a ∈ u := mem_u.2 ⟨hat, has, fun b hbs hbt ↦ (hm _ hbs hbt).trans hma⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a
have refine_2 : ∀ (a : α)
  (has :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
        Finset α)
      a)
  (hat :
    a ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)),
  a < w
Tactic: refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)
    a
hat :
  a ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
⊢ a < w
have refine_2 : ∀ (hwa : w ≤ a), False
Tactic: by_contra! hwa
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase (t.min' ⋯)) : Colex (Finset α))
have ht : t.Nonempty
Tactic: generalize_proofs ht
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have 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 α))
Tactic: obtain rfl | h' := eq_or_ne s t
Cleared hypotheses: t, hst, hcard, ht, m
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have 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 α))
Tactic: obtain rfl | h' := eq_or_ne s t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have hst₁ : 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'
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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 α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have hst₁ : ∃ 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
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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)
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have 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 α))
Tactic: obtain ⟨w, hwt, hws, hw⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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)
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have 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 α))
Tactic: obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_gt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have 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 α))
Tactic: obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_gt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have hma : m < a
Tactic: have hma : m < a := (min'_le _ _ hwt).trans_lt hwa
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
have inr : ∀ (b : α)
  (hbs :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := sorry : Finset α } : Finset α) b)
  (hbt :
    b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := sorry : Finset α } : Finset α)),
  b < a
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