awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)
⊢ b < a
have hbt₁ : b ∉ t.erase m
Tactic: change b ∉ t.erase m at hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t.erase m
⊢ b < a
have hbt₁ : b = m ∨ b ∉ t
Tactic: rw [mem_erase, not_and_or, not_ne_iff] at hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
⊢ b < a
have inr : ∀
  (hbs :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := sorry : Finset α } : Finset α) m),
  m < a
Tactic: obtain rfl | hbt := hbt
Cleared hypotheses: b, hbs, hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
inr :
  ∀
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m),
    m < a
⊢ b < a
have inr₁ : ∀ (hbt : b ∉ t), b < a
Tactic: obtain rfl | hbt := hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
⊢ b < a
have inr : ∀ (hab : a ≤ b), False
Tactic: by_contra! hab
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have inr : ∀ (hwt : m ∈ t) (hws : m ∉ s) (hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)) (haw : a < m),
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
Tactic: obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt
Cleared hypotheses: w, hwt, hws, hw, haw
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
inr :
  ∀ (hwt : m ∈ t) (hws : m ∉ s) (hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)) (haw : a < m),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have inr₁ : ∀ (hmw : m < w),
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
Tactic: obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
b : α
hb : b ∈ t.erase m
⊢ b ∈ s.erase a
have rw : ∀ (hb : b ≠ m ∧ b ∈ t), b ≠ a ∧ b ∈ s
Tactic: rw [mem_erase] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have this : t.erase m ⊆ s.erase a
Tactic: have : erase t m ⊆ erase s a := by
      rintro b hb
      rw [mem_erase] at hb ⊢
      exact ⟨(haw.trans_le <| min'_le _ _ hb.2).ne',
        (hw <| hb.1.lt_of_le' <| min'_le _ _ hb.2).2 hb.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have inr : #(s.erase a) ≤ #(t.erase m)
Tactic: rw [eq_of_subset_of_card_le this]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #(s.erase a) ≤ #(t.erase m)
have inr : #s - 1 ≤ #t - 1
Tactic: rw [card_erase_of_mem ha, card_erase_of_mem (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (t.erase m) : Colex (Finset α))
have inr : ∀ (b : α)
  (hbs :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := sorry : Finset α } : Finset α) b)
  (hbt :
    b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := sorry : Finset α } : Finset α)),
  b < w
Tactic: refine (lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws,
      fun b hbs hbt ↦ ?_⟩).le
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) { val := t.val.erase m, nodup := ⋯ : Finset α } : Finset α)
⊢ b < w
have hbt₁ : b ∉ t.erase m
Tactic: change b ∉ t.erase m at hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t.erase m
⊢ b < w
have hbt₁ : b = m ∨ b ∉ t
Tactic: rw [mem_erase, not_and_or, not_ne_iff] at hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
⊢ b < w
have inr : ∀
  (hbs :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := sorry : Finset α } : Finset α) m),
  m < w
Tactic: obtain rfl | hbt := hbt
Cleared hypotheses: b, hbs, hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b = m ∨ b ∉ t
inr :
  ∀
    (hbs :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) m),
    m < w
⊢ b < w
have inr₁ : ∀ (hbt : b ∉ t), b < w
Tactic: obtain rfl | hbt := hbt
Cleared hypotheses: hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α) { val := s.val.erase a, nodup := ⋯ : Finset α } : Finset α) b
hbt : b ∉ t
⊢ b < w
have inr : ∀ (hwb : w ≤ b), False
Tactic: by_contra! hwb
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
Tactic: simp_rw [← sdiff_eq_empty_iff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
have by_contra! : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
⊢ False
have have : ∀ (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁), False
Tactic: have ⟨⟨s, hs⟩, t, ht⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ \ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ \ 𝒜₁
⊢ False
have rw : ∀ (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
Tactic: rw [mem_sdiff] at hs ht
Cleared hypotheses: hs, t, ht
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
⊢ False
have inl : ∀
  (hst :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
  False
Tactic: obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
inl :
  ∀
    (hst :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
⊢ False
have inr : ∀
  (hst :
    Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
  False
Tactic: obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
inl :
  ∀
    (hst :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
inr :
  ∀
    (hst :
      Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
⊢ False
have inr₁ : ∀
  (hts :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))),
  False
Tactic: obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst :
  Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
⊢ False
have hst₁ : s = t
Tactic: simp only [toColex_inj] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have simp_rw₂ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁),
  False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
simp_rw₂ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁),
    False
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have simp_rw₃ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
  (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
simp_rw₂ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁),
    False
simp_rw₃ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have inl : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
  (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
  (hst :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
  False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
simp_rw₂ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁),
    False
simp_rw₃ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
inl :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
    (hst :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have inr : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
  (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
  (hst :
    Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
  False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
simp_rw₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
simp_rw₂ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁),
    False
simp_rw₃ :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
inl :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
    (hst :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
inr :
  ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
    (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
    (hst :
      Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))),
    False
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
have inr₁ : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty) (s : Finset α) (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α)
  (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁)
  (hts :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))),
  False
Tactic: classical
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩