awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ (b : α), s.min = (↑b : WithTop α)

Tactic:
let ⟨b, h, _⟩ := WithTop.le_iff_forall.1 (inf_le (α := WithTop α) h) _ rfl; ⟨b, h⟩

Premises used: _private.0.Finset.min_of_mem.match_1, WithTop.le_iff_forall, Exists, Finset.min, WithTop.some, Exists.intro, Iff.mp, Finset.inf_le, Eq, rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ ∃ (a : α), s.min = (↑a : WithTop α)

Tactic:
let ⟨_, h⟩ := h
  min_of_mem h

Premises used: Finset.min_of_mem, Exists, Finset.min, WithTop.some, _private.0.Finset.max_of_nonempty.match_1, Eq
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ s.min = ⊤ ↔ s = ∅

Tactic:
simp [Finset.min, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, Finset.min
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, s.min = (↑a : WithTop α) → a ∈ s

Tactic:
@mem_of_max αᵒᵈ _ s

Premises used: Set.Mem, setOf, Finset.min, WithTop.some, Finset.mem_of_max, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
as : a ∈ s
⊢ s.min ≤ (↑a : WithTop α)

Tactic:
inf_le as

Premises used: Finset.min, Finset.inf_le
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
h : (↑a : WithTop α) < s.min
⊢ a ∉ s

Tactic:
mt min_le h.not_ge

Premises used: Finset.min_le, mt, LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a b : α
h₁ : b ∈ s
h₂ : s.min = (↑a : WithTop α)
⊢ a ≤ b

Tactic:
WithTop.coe_le_coe.mp <| h₂.ge.trans (min_le h₁)

Premises used: Eq.ge, Finset.min_le, Iff.mp, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a b : α
h₁ : a < b
h₂ : s.min = (↑b : WithTop α)
⊢ a ∉ s

Tactic:
Finset.notMem_of_coe_lt_min <| (WithTop.coe_lt_coe.mpr h₁).trans_eq h₂.symm

Premises used: Iff.mpr, LT.lt.trans_eq, WithTop.coe_lt_coe, Finset.notMem_of_coe_lt_min, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
⊢ (s ∪ t).min = min s.min t.min

Tactic:
inf_union

Premises used: Finset.inf_union, Finset.min