awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ 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
have 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
Tactic: obtain rfl | hab := eq_or_ne a b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: obtain rfl | hab := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
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
have 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
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₂ : LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
  a ≤ b
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₃ : a ≤ b ↔ a ≤ b
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
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
have 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
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₂ : LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α)) ↔
  a ≤ b
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₃ : a ≤ b ↔ a ≤ b
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ 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
have 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
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α)) (insert a s) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (insert b s) : Colex (Finset α)) ↔
    a < b
have 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
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have rw₂ : a < b ↔ a < b
Tactic: rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
⊢ 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
have 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
Tactic: obtain rfl | hab := eq_or_ne a b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: obtain rfl | hab := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
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
have 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
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₂ : LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) {a} : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₃ : b ≤ a ↔ b ≤ a
Tactic: rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
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
have 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
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have 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
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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
have inr₂ : LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) {a} : 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]