awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
by_contra : ∀ (hat : a ∉ t), False
⊢ a ∈ t

Tactic:
by_contra hat
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
hat : a ∉ t
have : ∀ (_b : α) (hb₁ : _b ∈ s) (hb₂ : _b ∉ s), a ≤ _b → False
⊢ False

Tactic:
have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
hat : a ∉ t
_b : α
hb₁ : _b ∈ s
hb₂ : _b ∉ s
right : a ≤ _b
⊢ False

Tactic:
hb₂ hb₁
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
hat : a ∉ t
_b : α
hb₁ : _b ∈ s
hb₂ : _b ∉ s
right : a ≤ _b
⊢ False

Tactic:
exact hb₂ hb₁
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
pos :
  ∀ (hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
neg :
  ∀ (hat : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
by_cases hat : a ∈ ofColex t

Premises used: ofColex, DFunLike.coe
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
pos :
  ∀ (b : α) (hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b)
    (hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)) (hab : a ≤ b),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
have ⟨b, hbu, hbt, hab⟩ := htu hat hau
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
pos :
  ∀ (hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
neg :
  ∀ (hbs : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α)),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
by_cases hbs : b ∈ ofColex s

Premises used: ofColex, DFunLike.coe
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b
pos :
  ∀ (c : α) (hcu : c ∈ u) (hcs : c ∉ s) (hbc : b ≤ c),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b
c : α
hcu : c ∈ u
hcs : c ∉ s
hbc : b ≤ c
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
⟨c, hcu, hcs, hab.trans hbc⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b
c : α
hcu : c ∈ u
hcs : c ∉ s
hbc : b ≤ c
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
exact ⟨c, hcu, hcs, hab.trans hbc⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
⟨b, hbu, hbs, hab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
exact ⟨b, hbu, hbs, hab⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
trans_aux hst htu has hat

Premises used: _private.0.Finset.Colex.trans_aux
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
exact trans_aux hst htu has hat

Premises used: _private.0.Finset.Colex.trans_aux
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Colex (Finset α)
⊢ s ≤ t ↔
    ∀ ⦃a : α⦄,
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a →
        a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
          ∃ (b : α),
            Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) b ∧
              b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b

Tactic:
simp [lt_iff_le_and_ne, toColex_le_toColex, and_comm]

Premises used: lt_iff_le_and_ne, Finset.Colex.toColex_le_toColex, and_comm
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Monotone.{u_1, u_1} (α := Finset α) (β := Colex (Finset α)) (⇑toColex : (a : Finset α) → Colex (Finset α))

Tactic:
fun _s _t hst _a has hat ↦ (hat <| hst has).elim

Premises used: False.elim, Monotone
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ StrictMono.{u_1, u_1} (α := Finset α) (β := Colex (Finset α)) (⇑toColex : (a : Finset α) → Colex (Finset α))

Tactic:
toColex_mono.strictMono_of_injective toColex.injective

Premises used: Finset.Colex.toColex_mono, Monotone.strictMono_of_injective, toColex, Equiv.injective
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
h : s ⊆ t
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
toColex_mono h

Premises used: Finset.Colex.toColex_mono
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
h : s ⊂ t
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))

Tactic:
toColex_strictMono h

Premises used: Finset.Colex.toColex_strictMono
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t u : Finset α
a_1 b : α
s : Colex (Finset α)
a : α
ha :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) ∅ : Colex (Finset α)) :
      Finset α)
    a
⊢ a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) →
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b ∧
        b ∉
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) ∅ : Colex (Finset α)) :
              Finset α) ∧
          a ≤ b

Tactic:
cases ha
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) ∅ : Colex (Finset α))
    (⊥ : Colex (Finset α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) ⊥ : Finset α) (∅ : Finset α)

Tactic:
rfl

Premises used: Finset.empty, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
pos : b ∈ t → b ≤ a
neg : b ∉ t → b ≤ a
⊢ b ≤ a

Tactic:
by_cases b ∈ t
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∈ t
⊢ b ≤ a

Tactic:
ht _ ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∈ t
⊢ b ≤ a

Tactic:
exact ht _ ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∉ t
neg :
  ∀ (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hbc : b ≤ c), b ≤ a
⊢ b ≤ a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∉ t
c : α
hct :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    c
hbc : b ≤ c
⊢ b ≤ a

Tactic:
hbc.trans <| ht _ hct

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∉ t
c : α
hct :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    c
hbc : b ≤ c
⊢ b ≤ a

Tactic:
exact hbc.trans <| ht _ hct

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
pos : b ∈ t → b < a
neg : b ∉ t → b < a
⊢ b < a

Tactic:
by_cases b ∈ t
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∈ t
⊢ b < a

Tactic:
ht _ ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∈ t
⊢ b < a

Tactic:
exact ht _ ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∉ t
neg :
  ∀ (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hbc : b ≤ c), b < a
⊢ b < a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∉ t
c : α
hct :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    c
hbc : b ≤ c
⊢ b < a

Tactic:
hbc.trans_lt <| ht _ hct

Premises used: LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∉ t
c : α
hct :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
    c
hbc : b ≤ c
⊢ b < a

Tactic:
exact hbc.trans_lt <| ht _ hct

Premises used: LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
simp : (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
simp only [toColex_le_toColex, mem_singleton, exists_eq_left]

Premises used: Finset.mem_singleton, exists_eq_left, Finset.Colex.toColex_le_toColex
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
forall₂_congr fun b _ ↦ ?_

Premises used: forall₂_congr