awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : LE α
s_1 t_1 : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
mk :
  ∀ (carrier : Set α) (Chain' : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier)
    (max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier ⊆ s → carrier = s)
    (h : { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier = t.carrier),
    { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : LE α
s t_1 : Flag α
a : α
t : Flag α
carrier : Set α
Chain' : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier
max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier ⊆ s → carrier = s
h : { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier = t.carrier
mk :
  ∀ (carrier_1 : Set α) (Chain'_1 : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier_1)
    (max_chain'_1 : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier_1 ⊆ s → carrier_1 = s)
    (h :
      { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier =
        { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 : Flag α }.carrier),
    { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } =
      { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 }
⊢ { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } = t

Tactic:
cases t
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : LE α
s t : Flag α
a : α
carrier : Set α
Chain' : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier
max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier ⊆ s → carrier = s
carrier_1 : Set α
Chain'_1 : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier_1
max_chain'_1 : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier_1 ⊆ s → carrier_1 = s
h :
  { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier =
    { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 : Flag α }.carrier
⊢ { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } =
    { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s t : Flag α
⊢ (↑s : Set α) = (↑t : Set α) → s = t

Tactic:
SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s : Flag α
a : α
⊢ a ∈ (↑s : Set α) ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s : Set α
h₁ : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s_1 → s ⊆ s_1 → s = s_1
⊢ (↑{ carrier := s, Chain' := h₁, max_chain' := h₂ : Flag α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s : Flag α
⊢ { carrier := (↑s : Set α), Chain' := ⋯, max_chain' := ⋯ : Flag α } = s

Tactic:
ext rfl

Premises used: Flag.ext, rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s : Flag α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)

Tactic:
s.Chain'

Premises used: Flag.Chain'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
s : Flag α
⊢ IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)

Tactic:
⟨s.chain_le, s.max_chain'⟩

Premises used: Flag.max_chain', Flag.chain_le, IsMaxChain, And.intro
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
s : Flag α
⊢ ⊤ ∈ s

Tactic:
s.maxChain.top_mem

Premises used: IsMaxChain.top_mem, Flag.maxChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
s : Flag α
⊢ ⊥ ∈ s

Tactic:
s.maxChain.bot_mem

Premises used: IsMaxChain.bot_mem, Flag.maxChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : LE α
c : Set α
hc : IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
⊢ (↑(ofIsMaxChain c hc) : Set α) = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : Preorder α
a b : α
s : Flag α
ha : a ∈ s
hb : b ∈ s
⊢ a ≤ b ∨ b ≤ a

Tactic:
s.chain_le.total ha hb

Premises used: Flag.chain_le, IsChain.total
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : Preorder α
a : α
s : Flag α
⊢ a ∈ s ↔ ∀ ⦃b : α⦄, b ∈ s → a ≤ b ∨ b ≤ a

Tactic:
⟨fun ha b => s.le_or_le ha, fun hb =>
    of_not_not fun ha =>
      Set.ne_insert_of_notMem _ ‹_› <|
        s.maxChain.2 (s.chain_le.insert fun c hc _ => hb hc) <| Set.subset_insert _ _⟩

Premises used: Flag.chain_le, Flag.le_or_le, SetLike.coe, And.right, Iff.intro, Set.ne_insert_of_notMem, of_not_not, IsChain.insert, Set.subset_insert, Flag.maxChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Flag α
⊢ (↑((map e : (a : Flag α) → Flag β) s : Flag β) : Set β) = (⇑e : (a : α) → β) '' (↑s : Set α)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ (map e).symm = map e.symm

Tactic:
rfl

Premises used: Flag.ofIsMaxChain, Flag.map, Equiv.symm, rfl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : PartialOrder α
s : Flag α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 < x2) (↑s : Set α)

Tactic:
s.chain_le.lt_of_le

Premises used: Flag.chain_le, IsChain.lt_of_le
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
i : ι
⊢ MaximalFor (fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) f i

Tactic:
simp
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
i : ι
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) f i_1

Tactic:
exact ⟨i, by simp⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih : ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
cons :
  ∀ (j : ι) (hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j),
    ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ Finset.cons i s hi) f i_1
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ Finset.cons i s hi) f i_1

Tactic:
obtain ⟨j, hj⟩ := ih
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
pos : ∀ (hji : f j ≤ f i), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
neg : ∀ (hji : ¬f j ≤ f i), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1

Tactic:
by_cases hji : f j ≤ f i
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1

Tactic:
⟨i, mem_cons_self .., ?_⟩

Premises used: And.intro, Exists.intro, Finset.mem_cons_self
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
pos : ∀ ⦃j : ι⦄, (fun (x : ι) ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1

Tactic:
refine ⟨i, mem_cons_self .., ?_⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
pos : ∀ a ∈ s, f i ≤ f a → f a ≤ f i
⊢ ∀ ⦃j : ι⦄, (fun (x : ι) ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i

Tactic:
simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]

Premises used: forall_eq_or_imp, imp_self, Finset.mem_cons, true_and
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ a ∈ s, f i ≤ f a → f a ≤ f i

Tactic:
fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji

Premises used: trans, And.right
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ a ∈ s, f i ≤ f a → f a ≤ f i

Tactic:
exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji

Premises used: trans, And.right
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∀ ⦃j_1 : ι⦄, (fun (x : ι) ↦ x ∈ cons i s hi) j_1 → f j ≤ f j_1 → f j_1 ≤ f j

Tactic:
simpa [hji] using hj.2

Premises used: And.right
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1

Tactic:
exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : s.Nonempty
singleton : ∀ (i : ι), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) f i_1
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (hs : s.Nonempty) (ih : ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i),
    ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ Finset.cons i s hi) f i_1
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton i => exact ⟨i, by simp⟩
  | @cons i s hi hs ih =>
    obtain ⟨j, hj⟩ := ih
    by_cases hji : f j ≤ f i
    · refine ⟨i, mem_cons_self .., ?_⟩
      simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
      exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji
    · exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩

Premises used: Finset.cons, forall_eq_or_imp, imp_self, Singleton.singleton, Finset.mem_cons, true_and
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : s.Nonempty
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
exists_maximalFor (α := αᵒᵈ) f s hs

Premises used: Finset.exists_maximalFor, MinimalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
s : Finset α
hs : s.Nonempty
⊢ ∃ (i : α), Maximal (fun (x : α) ↦ x ∈ s) i

Tactic:
s.exists_maximalFor id hs

Premises used: id, Maximal, Finset.exists_maximalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
s : Finset α
hs : s.Nonempty
⊢ ∃ (i : α), Minimal (fun (x : α) ↦ x ∈ s) i

Tactic:
s.exists_minimalFor id hs

Premises used: Finset.exists_minimalFor, id, Minimal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ∈ s, a ≤ b ∧ ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b

Tactic:
simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩

Premises used: Iff.mpr, le_rfl, Finset.exists_maximal, And.intro, and_assoc, Exists.intro, Finset.mem_filter, Maximal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
obtain :
  ∀ (b : α) (hb : b ∈ s) (hab : a ≤ b) (hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b),
    ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b

Tactic:
obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b

Tactic:
⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b

Tactic:
exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
obtain : ∃ b ∈ s, a ≤ b ∧ ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
obtain₁ :
  ∀ (b : α) (hb : b ∈ s) (hab : a ≤ b) (hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b),
    ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b

Tactic:
classical
  obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ s) b

Tactic:
exists_le_maximal (α := αᵒᵈ) s ha

Premises used: Set.Mem, setOf, Finset.exists_le_maximal, OrderDual, Minimal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ s.Finite

Tactic:
h
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
lift : ∀ (s : Finset ι) (hs : (↑s : Set ι).Nonempty), ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ (↑s : Set ι)) f i
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
lift s to Finset ι using h

Premises used: Finset
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s : Set ι).Nonempty
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ (↑s : Set ι)) f i

Tactic:
s.exists_maximalFor f hs

Premises used: Finset.exists_maximalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s : Set ι).Nonempty
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ (↑s : Set ι)) f i

Tactic:
exact s.exists_maximalFor f hs

Premises used: Finset.exists_maximalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
Finite.exists_maximalFor (α := αᵒᵈ) f s h hs

Premises used: Set.Finite.exists_maximalFor, MinimalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
s : Set α
h : s.Finite
hs : s.Nonempty
⊢ ∃ (i : α), Maximal (fun (x : α) ↦ x ∈ s) i

Tactic:
h.exists_maximalFor id _ hs

Premises used: Set.Finite.exists_maximalFor, id, Maximal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
s : Set α
h : s.Finite
hs : s.Nonempty
⊢ ∃ (i : α), Minimal (fun (x : α) ↦ x ∈ s) i

Tactic:
h.exists_minimalFor id _ hs

Premises used: id, Set.Finite.exists_minimalFor, Minimal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
obtain :
  ∀ (a : ι) (ha : a ∈ s) (hmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)),
    ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximalFor id (f '' s) h (hs.image f)

Premises used: Set.Finite.exists_maximalFor, id, Set.Nonempty.image, Set.image, rfl
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
a : ι
ha : a ∈ s
hmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
⟨a, ha, fun a' ha' hf ↦ hmax (mem_image_of_mem f ha') hf⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
a : ι
ha : a ∈ s
hmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
exact ⟨a, ha, fun a' ha' hf ↦ hmax (mem_image_of_mem f ha') hf⟩
-- Module: Mathlib.Order.Preorder.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
h.exists_maximalFor' (α := αᵒᵈ) f s hs

Premises used: Set.Finite.exists_maximalFor', MinimalFor
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
lift : ∀ (s : Finset α) (ha : a ∈ (↑s : Set α)), ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ (↑s : Set α)) b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ (↑s : Set α)
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ (↑s : Set α)) b

Tactic:
s.exists_le_maximal ha

Premises used: Finset.exists_le_maximal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ (↑s : Set α)
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ (↑s : Set α)) b

Tactic:
exact s.exists_le_maximal ha

Premises used: Finset.exists_le_maximal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
lift : ∀ (s : Finset α) (ha : a ∈ (↑s : Set α)), ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ (↑s : Set α)) b
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ s) b

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ (↑s : Set α)
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ (↑s : Set α)) b

Tactic:
s.exists_le_minimal ha

Premises used: Finset.exists_le_minimal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ (↑s : Set α)
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ (↑s : Set α)) b

Tactic:
exact s.exists_le_minimal ha

Premises used: Finset.exists_le_minimal
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabit : ∀ (inhabited_h : Inhabited α), s.Infinite
⊢ s.Infinite

Tactic:
inhabit α
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
⊢ f 0 ∈ s

Tactic:
(h _).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, And.left
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
⊢ f 0 ∈ s

Tactic:
exact (h _).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
n : ℕ
⊢ f (n + 1) ∈ s

Tactic:
(h _).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, And.left
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
n : ℕ
⊢ f (n + 1) ∈ s

Tactic:
exact (h _).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite

Tactic:
infinite_of_injective_forall_mem
    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Premises used: strictMono_nat_of_lt_succ, StrictMono.injective, Set.infinite_of_injective_forall_mem
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite

Tactic:
exact infinite_of_injective_forall_mem
    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Premises used: strictMono_nat_of_lt_succ, StrictMono.injective, Set.infinite_of_injective_forall_mem
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, b < a
⊢ s.Infinite

Tactic:
infinite_of_forall_exists_gt (α := αᵒᵈ) h

Premises used: Set.infinite_of_forall_exists_gt, OrderDual
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : PartialOrder α
⊢ Set.Finite.{u_2} (α := α) {a : α | IsTop a}

Tactic:
(subsingleton_isTop α).finite

Premises used: Set.subsingleton_isTop, Set.Subsingleton.finite
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : PartialOrder α
⊢ Set.Finite.{u_2} (α := α) {a : α | IsBot a}

Tactic:
(subsingleton_isBot α).finite

Premises used: Set.subsingleton_isBot, Set.Subsingleton.finite