awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a_1 b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha :
  Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hamax :
  ∀ (x' : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) x' ∧
          x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) x' ∧
          x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
      id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s

Tactic:
ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)

Premises used: And.intro, Exists.intro, Or.inl, Or.imp, Or.inr
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a_1 b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha :
  Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hamax :
  ∀ (x' : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) x' ∧
          x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) x' ∧
          x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
      id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s

Tactic:
exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)

Premises used: Or.imp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
inl : t ≤ t ∨ t ≤ t
inr inr₁ : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
inr₂ :
  ∀ (hts : t ≠ s) (a : α)
    (ha :
      Membership.mem (γ := Finset α)
        (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
          Finset α)
        a)
    (hamax :
      ∀ (x' : α),
        Membership.mem (γ := Finset α)
            (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t)
                ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
              Finset α)
            x' →
          id x' ≤ id a),
    s ≤ t ∨ t ≤ s
inr₃ :
  ∀ (hts : t ≠ s) (a : α)
    (ha :
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
          a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
          a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α))
    (hamax :
      ∀ (x' : α),
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) x' ∧
              x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
            Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) x' ∧
              x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
          id x' ≤ id a),
    s ≤ t ∨ t ≤ s
⊢ s ≤ t ∨ t ≤ s

Tactic:
classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)

Premises used: eq_or_ne, Finset.mem_symmDiff, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
hst : s ≠ t
⊢ Finset.Nonempty.{u_1} (α := α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
rw : (∃ (x : α), ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
rw [← not_le, toColex_le_toColex, not_forall]

Premises used: not_le, Finset.Colex.toColex_le_toColex, Classical.not_forall
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ (∃ (x : α), ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
simp only [not_forall, not_exists, not_and, not_le, exists_prop]

Premises used: not_le, not_exists, exists_prop, not_and, Classical.not_forall
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
⊢ s < t ↔
    ∃ (a : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
        a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧
          ∀ (b : α),
            Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b →
              b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) → b < a

Tactic:
toColex_lt_toColex_iff_exists_forall_lt

Premises used: Set.Mem, setOf, Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
refine_1 :
  ∀
    (h :
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)))
    (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
refine_2 :
  ∀ (h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ 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 α)),
    ∃ (b : α),
      Membership.mem (γ := Finset α)
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
            Finset α)
          b ∧
        b ∉
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
              Finset α) ∧
          a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
refine_1 :
  let m := (s ∆ t).max' ⋯;
  m ∈ t
⊢ (s ∆ t).max' ⋯ ∈ t

Tactic:
set m := (s ∆ t).max' (symmDiff_nonempty.2 hst)

Premises used: Iff.mpr, Finset.max', Finset.symmDiff_nonempty, symmDiff
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
refine_1 : ∀ (hmt : m ∉ t), False
⊢ m ∈ t

Tactic:
by_contra hmt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ m ∈ s

Tactic:
simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst

Premises used: Iff.mpr, Finset.max'_mem, Finset.symmDiff_nonempty, Finset.mem_symmDiff
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ m ∈ s

Tactic:
have hms : m ∈ s := by
      simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
refine_1 :
  ∀ (b : α)
    (hbt :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        b)
    (hbs :
      b ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hmb : m ≤ b), False
⊢ False

Tactic:
have ⟨b, hbt, hbs, hmb⟩ := h hms hmt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
b : α
hbt :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    b
hbs :
  b ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)
hmb : m ≤ b
⊢ False

Tactic:
lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <|
      mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩

Premises used: Iff.mpr, lt_irrefl, ne_of_mem_of_not_mem, LE.le.lt_of_ne, And.intro, Iff.mp, Finset.mem_symmDiff, Finset.max'_lt_iff, Or.inr
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
b : α
hbt :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    b
hbs :
  b ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)
hmb : m ≤ b
⊢ False

Tactic:
exact lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <|
      mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩

Premises used: Iff.mpr, lt_irrefl, ne_of_mem_of_not_mem, LE.le.lt_of_ne, Iff.mp, Finset.mem_symmDiff, Finset.max'_lt_iff, Or.inr
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ 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 α)
⊢ s ≠ t

Tactic:
have hst : s ≠ t := ne_of_mem_of_not_mem' has hat
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ 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 α)
hst : s ≠ t
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        b ∧
      b ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        a ≤ b

Tactic:
⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩

Premises used: Iff.mpr, Finset.le_max', And.intro, Exists.intro, Finset.mem_symmDiff, Or.inl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ 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 α)
hst : s ≠ t
refine_2 :
  (s ∆ t).max' ⋯ ∉
    ((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 α)) t : Colex (Finset α)) :
          Finset α)
        b ∧
      b ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        a ≤ b

Tactic:
refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ 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 α)
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)

Tactic:
simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst

Premises used: Iff.mpr, Finset.max'_mem, Finset.symmDiff_nonempty, Finset.mem_symmDiff
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
⊢ s ≤ t ↔
    ∀ (h : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) ⋯)

Tactic:
toColex_le_toColex_iff_max'_mem

Premises used: Colex, Set.Mem, Finset.Colex.toColex_le_toColex_iff_max'_mem, setOf
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
rw :
  (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧
      Ne (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]

Premises used: lt_iff_le_and_ne, Finset.Colex.toColex_le_toColex_iff_max'_mem
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧
      Ne (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
rw :
  (∀ (h : s ≠ t),
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
          (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t)
            ⋯)) ∧
      s ≠ t ↔
    ∃ (_ : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) ⋯)
⊢ s < t ↔
    ∃ (_ : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) ⋯)

Tactic:
rw [lt_iff_le_and_ne, le_iff_max'_mem]

Premises used: lt_iff_le_and_ne, Finset.Colex.le_iff_max'_mem
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
⊢ (∀ (h : s ≠ t),
        Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
          (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t)
            ⋯)) ∧
      s ≠ t ↔
    ∃ (_ : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) ⋯)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
simp :
  (∃ (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)
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}

Tactic:
simp only [lt_iff_exists_forall_lt, mem_sdiff, filter_inj, and_assoc]

Premises used: Finset.Colex.lt_iff_exists_forall_lt, Finset.mem_sdiff, and_assoc, Finset.filter_inj
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ (∃ (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:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro