awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
⊢ StrictMono.{u_1, u_2} (β := Colex (Finset β)) fun (s : Colex (Finset α)) ↦
    (toColex : (a : Finset β) → Colex (Finset β)) (image f ((ofColex : (a : Colex (Finset α)) → Finset α) s))

Tactic:
fun _s _t ↦ (toColex_image_lt_toColex_image hf).2

Premises used: Iff.mpr, StrictMono, Set.Mem, setOf, Finset.Colex.toColex_image_lt_toColex_image
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Fintype α
⊢ Eq.{u_1 + 1} (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) univ : Colex (Finset α))
    (⊤ : Colex (Finset α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Fintype α
⊢ Eq.{u_1 + 1} (α := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) ⊤ : Finset α) (univ : Finset α)

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
r : ℕ
⊢ IsInitSeg.{u_1} (α := α) ∅ r

Tactic:
simp [IsInitSeg]

Premises used: Finset.Colex.IsInitSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
simp_rw : 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

Tactic:
simp_rw [← sdiff_eq_empty_iff_subset]

Premises used: Finset.sdiff_eq_empty_iff_subset
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
by_contra! : ∀ (h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty), False
⊢ 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
have : ∀ (s : Finset α) (hs : s ∈ 𝒜₁ \ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ \ 𝒜₁), False
⊢ False

Tactic:
have ⟨⟨s, hs⟩, t, ht⟩ := h
-- Module: Mathlib.Combinatorics.Colex
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 ∈ 𝒜₂ \ 𝒜₁
rw : ∀ (hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂) (t : Finset α) (ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁), False
⊢ False

Tactic:
rw [mem_sdiff] at hs ht

Premises used: Finset.mem_sdiff
-- Module: Mathlib.Combinatorics.Colex
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
inr₁ :
  ∀
    (hts :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))),
    False
⊢ False

Tactic:
obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)

Premises used: LT.lt, toColex, trichotomous_of, DFunLike.coe
-- Module: Mathlib.Combinatorics.Colex
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 :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
⊢ False

Tactic:
hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
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 :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
⊢ False

Tactic:
exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
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 α))
⊢ s = t

Tactic:
simp only [toColex_inj] at hst

Premises used: toColex_inj
-- Module: Mathlib.Combinatorics.Colex
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 : s = t
⊢ False

Tactic:
ht.2 <| hst ▸ hs.1

Premises used: Eq.rec, And.right, And.left
-- Module: Mathlib.Combinatorics.Colex
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 : s = t
⊢ False

Tactic:
exact ht.2 <| hst ▸ hs.1

Premises used: And.right
-- Module: Mathlib.Combinatorics.Colex
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 ∉ 𝒜₁
hts :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ False

Tactic:
ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
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 ∉ 𝒜₁
hts :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ False

Tactic:
exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
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
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
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
inr₃ 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⟩

Premises used: Finset.mem_sdiff, toColex_inj, Finset.sdiff_eq_empty_iff_subset
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
inst_1 : Fintype α
⊢ t ∈ initSeg s ↔
    #s = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))

Tactic:
simp [initSeg]

Premises used: Finset.Colex.initSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
⊢ s ∈ initSeg s

Tactic:
simp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
⊢ (initSeg s).Nonempty

Tactic:
⟨s, mem_initSeg_self⟩

Premises used: Finset.Colex.mem_initSeg_self, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
⊢ IsInitSeg (initSeg s) #s

Tactic:
⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩

Premises used: Iff.mpr, Finset.Colex.mem_initSeg, And.right, And.left, And.intro, Iff.mp, Finset.Colex.IsInitSeg, Eq.symm
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
refine :
  ∀ (t₁ t₂ : Finset α) (ht₁ : t₁ ∈ initSeg s)
    (ht₂ :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
        #t₂ = #s),
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ IsInitSeg (initSeg s) #s

Tactic:
refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s
⊢ #s = #t₁ ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))

Tactic:
rw [mem_initSeg] at ht₁

Premises used: Finset.Colex.mem_initSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s
ht₃ :
  #s = #t₁ ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s

Tactic:
rw [mem_initSeg] at ht₁

Premises used: Finset.Colex.mem_initSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
t₁ t₂ : Finset α
ht₁ :
  #s = #t₁ ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
ht₂ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))

Tactic:
ht₂.1.le.trans ht₁.2

Premises used: LT.lt.le, And.right, And.left, LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
t₁ t₂ : Finset α
ht₁ :
  #s = #t₁ ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
ht₂ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))

Tactic:
exact ht₂.1.le.trans ht₁.2

Premises used: LT.lt.le, And.right, And.left, LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
a : Finset α
ha : a ∈ 𝒜
⊢ Membership.mem (α := Colex (Finset α)) (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    ((toColex : (a : Finset α) → Colex (Finset α)) a : Colex (Finset α))

Tactic:
simpa using ha
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
⊢ Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))

Tactic:
have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex
    (fun a ha ↦ by simpa using ha)
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
⊢ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s

Tactic:
⟨_, h𝒜.1 hs, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
refine : 𝒜 = initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
⊢ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨_, h𝒜.1 hs, ?_⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
h :
  ∀ (t : Finset α),
    t ∈ 𝒜 ↔
      Membership.mem (γ := Finset (Finset α)) (initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))) t
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))

Tactic:
ext t
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
h :
  t ∈ 𝒜 ↔
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))
⊢ t ∈ 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))) t

Tactic:
rw [mem_initSeg]

Premises used: Finset.Colex.mem_initSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
⊢ t ∈ 𝒜 ↔
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))

Tactic:
⟨fun p ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
h :
  ∀ (p : t ∈ 𝒜),
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))
h₁ :
  card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α)) →
    t ∈ 𝒜
⊢ t ∈ 𝒜 ↔
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))

Tactic:
refine ⟨fun p ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
p : t ∈ 𝒜
h :
  r = r ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
        Colex (Finset α))
⊢ card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
        Colex (Finset α))

Tactic:
rw [h𝒜.1 p, h𝒜.1 hs]

Premises used: And.left
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
p : t ∈ 𝒜
⊢ r = r ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
        Colex (Finset α))

Tactic:
⟨rfl, le_sup' _ p⟩

Premises used: And.intro, Finset.le_sup', rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
p : t ∈ 𝒜
⊢ r = r ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
        Colex (Finset α))

Tactic:
exact ⟨rfl, le_sup' _ p⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
cards : card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t
le :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
h :
  ∀
    (p :
      Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))),
    t ∈ 𝒜
h₁ :
  ∀
    (p :
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
          Colex (Finset α))),
    t ∈ 𝒜
⊢ t ∈ 𝒜

Tactic:
obtain p | p := le.eq_or_lt

Premises used: LE.le.eq_or_lt