awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
refine : ∀ b ∈ s, ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
refine forall₂_congr fun b _ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
h : b ∈ s
inl : ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)
inr : ∀ (hba : b ≠ a), ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
obtain rfl | hba := eq_or_ne b a

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
b : α
h : b ∈ s
⊢ ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
h : b ∈ s
hba : b ≠ a
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
rw : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    ∀ b ∈ s, b < a

Tactic:
rw [lt_iff_le_and_ne, toColex_le_singleton, ne_eq, toColex_inj]

Premises used: Finset.Colex.toColex_le_singleton, lt_iff_le_and_ne, ne_eq, toColex_inj
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a

Tactic:
⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩

Premises used: lt_irrefl, False.elim, LT.lt.le, LE.le.lt_of_ne, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
refine_1 : ∀ (h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}) (b : α) (hb : b ∈ s), b ≠ a
refine_2 : ∀ (h : ∀ b ∈ s, b < a), ¬s = {a}
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a

Tactic:
refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ ¬s = {b}
⊢ False

Tactic:
h.2 <| eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc ↦ (h.1 _ hc).2 hb⟩

Premises used: Iff.mpr, Finset.eq_singleton_iff_unique_mem, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ ¬s = {b}
⊢ False

Tactic:
refine h.2 <| eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc ↦ (h.1 _ hc).2 hb⟩

Premises used: Iff.mpr, Finset.eq_singleton_iff_unique_mem, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
a : α
h : ∀ (b : α), Membership.mem (γ := Finset α) {a} b → b < a
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
simp : (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) ↔
    ∃ x ∈ s, a ≤ x

Tactic:
simp [toColex_le_toColex]

Premises used: Finset.Colex.toColex_le_toColex
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
pos : a ∈ s → ((a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x)
neg : a ∉ s → ((a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x)
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
by_cases a ∈ s
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
h : a ∈ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
h : a ∉ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
    a ≤ b

Tactic:
simp [toColex_le_singleton, eq_comm]

Premises used: Finset.Colex.toColex_le_singleton, eq_comm
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
    a < b

Tactic:
simp [toColex_lt_singleton]

Premises used: Finset.Colex.toColex_lt_singleton
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Colex (Finset α)
⊢ s ≤ t ↔
    (↑((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) : Set α) \
        (↑((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) : Set α) ⊆
      (↑(lowerClosure
            ((↑((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) : Set α) \
              (↑((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) : Set α))) :
        Set α)

Tactic:
simp [le_def, Set.subset_def, and_assoc]

Premises used: Set.subset_def, Finset.Colex.le_def, and_assoc
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₁ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₂ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ (b : α), (b ∈ t \ u ∧ b ∉ s \ u) ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ (b : α), (b ∈ t ∧ b ∉ s) ∧ a ≤ b
simp_rw₃ :
  (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ (t \ u) \ (s \ u), a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
simp_rw₄ : (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ t \ s, a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]

Premises used: and_imp, Finset.Colex.toColex_le_toColex, Finset.mem_sdiff, and_assoc, sdiff_sdiff_sdiff_cancel_right
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : 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_sdiff_le_toColex_sdiff hut hus) <|
    toColex_sdiff_le_toColex_sdiff hus hut

Premises used: Finset.Colex.toColex_sdiff_le_toColex_sdiff, lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
inst_1 : DecidableEq α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ t) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ s) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
simpa using toColex_sdiff_le_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Premises used: Finset.inter_subset_right, Finset.Colex.toColex_sdiff_le_toColex_sdiff, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
inst_1 : DecidableEq α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ t) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ s) : Colex (Finset α)) ↔
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Premises used: Finset.inter_subset_right, Finset.Colex.toColex_sdiff_lt_toColex_sdiff, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
inl :
  ∀ (hb : a ∉ s),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s hb) : Colex (Finset α)) ↔
      a ≤ a
inr :
  ∀ (hab : a ≠ b),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
      a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a ≤ b

Tactic:
obtain rfl | hab := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
ha hb : a ∉ s
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s hb) : Colex (Finset α)) ↔
    a ≤ a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
inr :
  LE.le (α := Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha \ cons b s hb) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb \ cons a s ha) : Colex (Finset α)) ↔
    a ≤ b
inr₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb \ cons a s ha) : Colex (Finset α)) ↔
    a ≤ b
inr₂ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
    a ≤ b
inr₃ inr₄ : a ≤ b ↔ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a ≤ b

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

Premises used: Finset.Colex.toColex_sdiff_le_toColex_sdiff', Ne.symm, Finset.Colex.singleton_le_singleton, Finset.cons_sdiff_cons
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
inr :
  LE.le (α := Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha \ cons b s hb) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb \ cons a s ha) : Colex (Finset α)) ↔
    a ≤ b
inr₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb \ cons a s ha) : Colex (Finset α)) ↔
    a ≤ b
inr₂ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
    a ≤ b
inr₃ inr₄ : a ≤ b ↔ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a ≤ b

Tactic:
classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

Premises used: Finset.Colex.toColex_sdiff_le_toColex_sdiff', Finset.Colex.singleton_le_singleton
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a < b

Tactic:
lt_iff_lt_of_le_iff_le' (cons_le_cons _ _) (cons_le_cons _ _)

Premises used: lt_iff_lt_of_le_iff_le', Finset.Colex.cons_le_cons
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∉ s
hb : b ∉ s
rw :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (insert b s) : Colex (Finset α)) ↔
    a ≤ b
rw₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a s) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (insert b s) : Colex (Finset α)) ↔
    a ≤ b

Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]

Premises used: Finset.cons_eq_insert, Finset.Colex.cons_le_cons
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∉ s
hb : b ∉ s
rw :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (insert b s) : Colex (Finset α)) ↔
    a < b
rw₁ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (cons a s ha) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (cons b s hb) : Colex (Finset α)) ↔
    a < b
rw₂ rw₃ : a < b ↔ a < b
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a s) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (insert b s) : Colex (Finset α)) ↔
    a < b

Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]

Premises used: Finset.Colex.cons_lt_cons, Finset.cons_eq_insert
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
inl :
  ∀ (hb : a ∈ s),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α)) ↔
      a ≤ a
inr :
  ∀ (hab : a ≠ b),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
      b ≤ a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
    b ≤ a

Tactic:
obtain rfl | hab := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
inst_1 : DecidableEq α
ha hb : a ∈ s
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α)) ↔
    a ≤ a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
inr :
  LE.le (α := Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a \ s.erase b) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₂ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    b ≤ a
inr₃ inr₄ : b ≤ a ↔ b ≤ a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
    b ≤ a

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]

Premises used: Finset.Colex.toColex_sdiff_le_toColex_sdiff', Ne.symm, Finset.erase_sdiff_erase, Finset.Colex.singleton_le_singleton
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
inr :
  LE.le (α := Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a \ s.erase b) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₂ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    b ≤ a
inr₃ inr₄ : b ≤ a ↔ b ≤ a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
    b ≤ a

Tactic:
classical
  rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]

Premises used: Finset.Colex.toColex_sdiff_le_toColex_sdiff', Ne.symm, Finset.erase_sdiff_erase, Finset.Colex.singleton_le_singleton
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
    b < a

Tactic:
lt_iff_lt_of_le_iff_le' (erase_le_erase hb ha) (erase_le_erase ha hb)

Premises used: Finset.Colex.erase_le_erase, lt_iff_lt_of_le_iff_le'
-- 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 : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
⊢ s ≤ t ∨ t ≤ s

Tactic:
obtain rfl | hts := eq_or_ne t s

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t_1 u : Finset α
a b : α
r : ℕ
t : Colex (Finset α)
⊢ t ≤ t ∨ t ≤ t

Tactic:
simp
-- 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 α)
hts : t ≠ s
inr :
  ∀ (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
⊢ s ≤ t ∨ t ≤ s

Tactic:
have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
-- 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 α)
    (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
⊢ 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 α)

Tactic:
simp_rw [mem_symmDiff] at ha hamax

Premises used: Finset.mem_symmDiff
-- 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 α)
    (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
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 α)
⊢ ∀ (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

Tactic:
simp_rw [mem_symmDiff] at ha hamax

Premises used: Finset.mem_symmDiff