awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
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)
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
⊢ (∃ (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)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Colex
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 : α
⊢ w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w

Tactic:
simp [u, and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Combinatorics.Colex
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 : α}, 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]
-- Module: Mathlib.Combinatorics.Colex
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
⊢ u.Nonempty

Tactic:
have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2
-- Module: Mathlib.Combinatorics.Colex
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
⊢ m ∈ t

Tactic:
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
-- Module: Mathlib.Combinatorics.Colex
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
⊢ m ∉ s

Tactic:
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
-- Module: Mathlib.Combinatorics.Colex
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
⊢ ∀ 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 _ _
-- Module: Mathlib.Combinatorics.Colex
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)

Tactic:
⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩

Premises used: not_imp_comm, LT.lt.asymm, And.intro, Iff.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
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
refine_1 : ∀ (a : α) (hma : m < a) (hat : a ∈ t), a ∈ s
⊢ ∃ 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 ↦ ?_⟩⟩
-- Module: Mathlib.Combinatorics.Colex
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
refine_1 : ∀ (has : a ∉ s), False
⊢ a ∈ s

Tactic:
by_contra has
-- Module: Mathlib.Combinatorics.Colex
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
⊢ a ∈ u

Tactic:
have hau : a ∈ u := mem_u.2 ⟨hat, has, fun b hbs hbt ↦ (hm _ hbs hbt).trans hma⟩
-- Module: Mathlib.Combinatorics.Colex
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
hau : a ∈ u
⊢ False

Tactic:
hma.not_ge <| le_max' _ _ hau

Premises used: Finset.le_max', LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Colex
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
hau : a ∈ u
⊢ False

Tactic:
exact hma.not_ge <| le_max' _ _ hau

Premises used: Finset.le_max', LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Colex
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

Tactic:
⟨w, hwt, hws, fun a has hat ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
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
⊢ ∃ (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 ⟨w, hwt, hws, fun a has hat ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Colex
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 α)
refine_2 : ∀ (hwa : w ≤ a), False
⊢ a < w

Tactic:
by_contra! hwa
-- Module: Mathlib.Combinatorics.Colex
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 α)
hwa : w ≤ a
⊢ False

Tactic:
hat <| (hw <| hwa.lt_of_ne <| ne_of_mem_of_not_mem hwt hat).1 has

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
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 α)
hwa : w ≤ a
⊢ False

Tactic:
exact hat <| (hw <| hwa.lt_of_ne <| ne_of_mem_of_not_mem hwt hat).1 has

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, Iff.mp
-- 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
⊢ t.Nonempty

Tactic:
generalize_proofs ht
-- 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
set :
  let 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 α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase (t.min' ht)) : Colex (Finset α))

Tactic:
set m := min' t ht

Premises used: Finset.min'