awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
st : s ⊆ t
⊢ t.min ≤ s.min

Tactic:
inf_mono st

Premises used: Finset.min, Finset.inf_mono
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
m : WithTop α
s : Finset α
st : ∀ a ∈ s, m ≤ (↑a : WithTop α)
⊢ m ≤ s.min

Tactic:
Finset.le_inf st

Premises used: Finset.min, Finset.le_inf
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
m : WithTop α
s : Finset α
⊢ m ≤ s.min ↔ ∀ a ∈ s, m ≤ (↑a : WithTop α)

Tactic:
Finset.le_inf_iff

Premises used: Finset.min, Finset.le_inf_iff
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset α
⊢ s.min = ⊥ ↔ ⊥ ∈ s

Tactic:
Finset.max_eq_top (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Finset.min, WithTop.some, Finset.max_eq_top, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min = (↑(s.min' H) : WithTop α)

Tactic:
simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

Premises used: Finset.min', Finset.coe_inf', Finset.min, Function.comp_def, id_eq
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
x : α
H2 : x ∈ s
⊢ s.min' ⋯ ≤ x

Tactic:
min_le_of_eq H2 (WithTop.coe_untop _ _).symm

Premises used: WithTop.coe_untop, Finset.min_le_of_eq, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
H2 : ∀ y ∈ s, x ≤ y
⊢ x ≤ s.min' H

Tactic:
H2 _ <| min'_mem _ _

Premises used: Finset.min'_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑s : Set α) (s.min' H)

Tactic:
⟨min'_mem _ _, min'_le _⟩

Premises used: Finset.min'_le, Finset.min'_mem, IsLeast, And.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
⊢ x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y

Tactic:
le_isGLB_iff (isLeast_min' s H).isGLB

Premises used: lowerBounds, Set.Mem, setOf, IsLeast.isGLB, le_isGLB_iff, Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ min' {a} ⋯ = a

Tactic:
simp [min']

Premises used: Finset.min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.max = (↑(s.max' H) : WithBot α)

Tactic:
simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]

Premises used: Finset.max', Finset.coe_sup', Function.comp_def, Finset.max, id_eq
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
x : α
H2 : x ∈ s
⊢ x ≤ s.max' ⋯

Tactic:
le_max_of_eq H2 (WithBot.coe_unbot _ _).symm

Premises used: WithBot.coe_unbot, Finset.le_max_of_eq, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
H2 : ∀ y ∈ s, y ≤ x
⊢ s.max' H ≤ x

Tactic:
H2 _ <| max'_mem _ _

Premises used: Finset.max'_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑s : Set α) (s.max' H)

Tactic:
⟨max'_mem _ _, le_max' _⟩

Premises used: Finset.max'_mem, IsGreatest, Finset.le_max', And.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
⊢ s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x

Tactic:
isLUB_le_iff (isGreatest_max' s H).isLUB

Premises used: Set.Mem, setOf, Finset.isGreatest_max', upperBounds, isLUB_le_iff, IsGreatest.isLUB
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
⊢ s.max' H < x ↔ ∀ y ∈ s, y < x

Tactic:
⟨fun Hlt y hy => (s.le_max' y hy).trans_lt Hlt, fun H => H _ <| s.max'_mem _⟩

Premises used: Finset.max'_mem, Finset.max', Finset.le_max', Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
⊢ x < s.min' H ↔ ∀ y ∈ s, x < y

Tactic:
@max'_lt_iff αᵒᵈ _ _ H _

Premises used: Finset.min', Finset.inf', Set.Mem, setOf, WithTop.some, WithTop.untop, OrderDual, Finset.inf, Finset.max'_lt_iff, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.max' H = s.sup' H id

Tactic:
rfl

Premises used: Finset.max', rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min' H = s.inf' H id

Tactic:
rfl

Premises used: Finset.min', rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ max' {a} ⋯ = a

Tactic:
simp [max']

Premises used: Finset.max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
a : α
⊢ s.min' H = a ↔ a ∈ s ∧ ∀ b ∈ s, a ≤ b

Tactic:
⟨(· ▸ ⟨min'_mem _ _, min'_le _⟩), fun h ↦ le_antisymm (min'_le _ _ h.1) (le_min' _ _ _ h.2)⟩

Premises used: Finset.min'_le, Finset.min'_mem, Eq.rec, le_antisymm, And.right, And.left, And.intro, Iff.intro, Finset.le_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
a : α
⊢ s.max' H = a ↔ a ∈ s ∧ ∀ b ∈ s, b ≤ a

Tactic:
⟨(· ▸ ⟨max'_mem _ _, le_max' _⟩), fun h ↦ le_antisymm (max'_le _ _ _ h.2) (le_max' _ _ h.1)⟩

Premises used: Finset.max'_le, Finset.max'_mem, Eq.rec, le_antisymm, And.right, And.left, Finset.le_max', And.intro, Iff.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.min' hs ≤ s.max' hs

Tactic:
min'_le _ _ (max'_mem _ _)

Premises used: Finset.min'_le, Finset.max'_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
i j : α
H1 : i ∈ s
H2 : j ∈ s
H3 : i ≠ j
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
isGLB_lt_isLUB_of_ne (s.isLeast_min' _).isGLB (s.isGreatest_max' _).isLUB H1 H2 H3

Premises used: IsLeast.isGLB, Finset.isGreatest_max', IsGreatest.isLUB, isGLB_lt_isLUB_of_ne, Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
h₂ : 1 < #s
⊢ 0 < #s

Tactic:
lia
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h₂ : 1 < #s
rcases : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s) (hab : a ≠ b), s.min' ⋯ < s.max' ⋯
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩

Premises used: Iff.mp, Finset.one_lt_card
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h₂ : 1 < #s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
s.min'_lt_max' ha hb hab

Premises used: Finset.min'_lt_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h₂ : 1 < #s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
exact s.min'_lt_max' ha hb hab

Premises used: Finset.min'_lt_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s₁ s₂ : Finset α
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
⊢ (s₁ ∪ s₂).max' ⋯ = max (s₁.max' h₁) (s₂.max' h₂)

Tactic:
sup'_union h₁ h₂ id

Premises used: Finset.max', id, Finset.sup'_union
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s₁ s₂ : Finset α
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
⊢ (s₁ ∪ s₂).min' ⋯ = min (s₁.min' h₁) (s₂.min' h₂)

Tactic:
inf'_union h₁ h₂ id

Premises used: Finset.min', id, Finset.inf'_union
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
rw :
  Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (s.sup (WithBot.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))
⊢ Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (Finset.max (image (⇑ofDual : (a : αᵒᵈ) → α) s))

Tactic:
rw [max_eq_sup_withBot, sup_image]

Premises used: Finset.max_eq_sup_withBot, Finset.sup_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (s.sup (WithBot.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))

Tactic:
congr_fun WithBot.map_id _

Premises used: Multiset.foldr, WithBot.some, WithBot, Finset.fold, WithTop.map, Finset.min, Finset.sup, congr_fun, OrderDual, Finset.inf, WithBot.map_id, Multiset.fold, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (s.sup (WithBot.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))

Tactic:
exact congr_fun WithBot.map_id _

Premises used: congr_fun, WithBot.map_id
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
rw :
  Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (s.inf (WithTop.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))
⊢ Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (Finset.min (image (⇑ofDual : (a : αᵒᵈ) → α) s))

Tactic:
rw [min_eq_inf_withTop, inf_image]

Premises used: Finset.min_eq_inf_withTop, Finset.inf_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (s.inf (WithTop.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))

Tactic:
congr_fun WithTop.map_id _

Premises used: Multiset.foldr, WithBot, WithTop.map_id, Finset.fold, WithTop.some, Finset.max, Finset.sup, congr_fun, OrderDual, Finset.inf, WithBot.map, Multiset.fold, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (s.inf (WithTop.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))

Tactic:
exact congr_fun WithTop.map_id _

Premises used: WithTop.map_id, congr_fun
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
rw :
  Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (s.sup (WithBot.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))
⊢ Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (Finset.max (image (⇑toDual : (a : α) → αᵒᵈ) s))

Tactic:
rw [max_eq_sup_withBot, sup_image]

Premises used: Finset.max_eq_sup_withBot, Finset.sup_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (s.sup (WithBot.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))

Tactic:
congr_fun WithBot.map_id _

Premises used: Multiset.foldr, WithBot.some, WithBot, Finset.fold, WithTop.map, Finset.min, Finset.sup, congr_fun, OrderDual, Finset.inf, WithBot.map_id, Multiset.fold, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (s.sup (WithBot.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))

Tactic:
exact congr_fun WithBot.map_id _

Premises used: congr_fun, WithBot.map_id
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
rw :
  Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (s.inf (WithTop.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))
⊢ Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (Finset.min (image (⇑toDual : (a : α) → αᵒᵈ) s))

Tactic:
rw [min_eq_inf_withTop, inf_image]

Premises used: Finset.min_eq_inf_withTop, Finset.inf_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (s.inf (WithTop.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))

Tactic:
congr_fun WithTop.map_id _

Premises used: Multiset.foldr, WithBot, WithTop.map_id, Finset.fold, WithTop.some, Finset.max, Finset.sup, congr_fun, OrderDual, Finset.inf, WithBot.map, Multiset.fold, WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (s.inf (WithTop.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))

Tactic:
exact congr_fun WithTop.map_id _

Premises used: WithTop.map_id, congr_fun
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (s.min' hs) : α) (max' (image (⇑ofDual : (a : αᵒᵈ) → α) s) ⋯ : α)

Tactic:
simp [min'_eq_inf', max'_eq_sup']

Premises used: Finset.max'_eq_sup', Finset.min'_eq_inf'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (s.max' hs) : α) (min' (image (⇑ofDual : (a : αᵒᵈ) → α) s) ⋯ : α)

Tactic:
simp [min'_eq_inf', max'_eq_sup']

Premises used: Finset.max'_eq_sup', Finset.min'_eq_inf'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (s.min' hs) : αᵒᵈ) (max' (image (⇑toDual : (a : α) → αᵒᵈ) s) ⋯ : αᵒᵈ)

Tactic:
simp [min'_eq_inf', max'_eq_sup']

Premises used: Finset.max'_eq_sup', Finset.min'_eq_inf'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (s.max' hs) : αᵒᵈ) (min' (image (⇑toDual : (a : α) → αᵒᵈ) s) ⋯ : αᵒᵈ)

Tactic:
simp [min'_eq_inf', max'_eq_sup']

Premises used: Finset.max'_eq_sup', Finset.min'_eq_inf'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
H : s.Nonempty
hst : s ⊆ t
⊢ s.max' H ≤ t.max' ⋯

Tactic:
le_max' _ _ (hst (s.max'_mem H))

Premises used: Finset.max'_mem, Finset.le_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
H : s.Nonempty
hst : s ⊆ t
⊢ t.min' ⋯ ≤ s.min' H

Tactic:
min'_le _ _ (hst (s.min'_mem H))

Premises used: Finset.min'_le, Finset.min'_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
rw : IsGreatest (insert a (↑s : Set α)) (max a (s.max' H))
⊢ IsGreatest (↑(insert a s) : Set α) (max a (s.max' H))

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a (↑s : Set α)) (max a (s.max' H))

Tactic:
(isGreatest_max' _ _).insert _

Premises used: IsGreatest.insert, Finset.isGreatest_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a (↑s : Set α)) (max a (s.max' H))

Tactic:
exact (isGreatest_max' _ _).insert _

Premises used: IsGreatest.insert, Finset.isGreatest_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
rw : IsLeast (insert a (↑s : Set α)) (min a (s.min' H))
⊢ IsLeast (↑(insert a s) : Set α) (min a (s.min' H))

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a (↑s : Set α)) (min a (s.min' H))

Tactic:
(isLeast_min' _ _).insert _

Premises used: IsLeast.insert, Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a (↑s : Set α)) (min a (s.min' H))

Tactic:
exact (isLeast_min' _ _).insert _

Premises used: IsLeast.insert, Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ min' {a, b} ⋯ = min a b

Tactic:
simp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ max' {a, b} ⋯ = max a b

Tactic:
simp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
inst_1 : DecidableEq α
a : α
ha : a ∈ s.erase (s.max' H)
⊢ a < s.max' H

Tactic:
lt_of_le_of_ne (le_max' _ _ (mem_of_mem_erase ha)) <| ne_of_mem_of_not_mem ha <| notMem_erase _ _

Premises used: ne_of_mem_of_not_mem, Finset.le_max', Finset.mem_of_mem_erase, Finset.notMem_erase, lt_of_le_of_ne
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
H : s.Nonempty
inst_1 : DecidableEq α
a : α
ha : a ∈ s.erase (s.min' H)
⊢ s.min' H < a

Tactic:
@lt_max'_of_mem_erase_max' αᵒᵈ _ s H _ a ha

Premises used: Finset.min', Finset.inf', WithTop.some, WithTop.untop, OrderDual, Finset.inf, Finset.lt_max'_of_mem_erase_max', WithTop
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
simp : s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)
⊢ (image f s).max' h = f (s.max' ⋯)

Tactic:
simp only [max', sup'_image]

Premises used: Finset.sup'_image, Finset.max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)

Tactic:
.symm <| comp_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

Premises used: Monotone.map_max, Finset.comp_sup'_eq_sup'_comp, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)

Tactic:
exact .symm <| comp_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

Premises used: Monotone.map_max, Finset.comp_sup'_eq_sup'_comp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : s.Nonempty
⊢ f (s.max' h) = (image f s).max' ⋯

Tactic:
.symm <| max'_image hf ..

Premises used: Finset.max'_image, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
simp : s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
simp only [min', inf'_image]

Premises used: Finset.min', Finset.inf'_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)

Tactic:
.symm <| comp_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

Premises used: Finset.comp_inf'_eq_inf'_comp, Monotone.map_min, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)

Tactic:
exact .symm <| comp_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

Premises used: Finset.comp_inf'_eq_inf'_comp, Monotone.map_min
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : s.Nonempty
⊢ f (s.min' h) = (image f s).min' ⋯

Tactic:
.symm <| min'_image hf ..

Premises used: Finset.min'_image, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ (↑(s.max' hs) : WithBot α) = s.max

Tactic:
coe_sup' hs id

Premises used: WithBot.some, Finset.max', Finset.coe_sup', id, Finset.max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ (↑(s.min' hs) : WithTop α) = s.min

Tactic:
coe_inf' hs id

Premises used: Finset.min', Finset.coe_inf', Finset.min, id, WithTop.some
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.max ∈ image WithBot.some s

Tactic:
mem_image.2 ⟨max' s hs, max'_mem _ _, coe_max' hs⟩

Premises used: Iff.mpr, Finset.mem_image, Finset.max'_mem, Finset.max', And.intro, Exists.intro, Finset.coe_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.min ∈ image WithTop.some s

Tactic:
mem_image.2 ⟨min' s hs, min'_mem _ _, coe_min' hs⟩

Premises used: Finset.min', Iff.mpr, Finset.mem_image, Finset.min'_mem, Finset.coe_min', And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ s.max ∈ insert ⊥ (image WithBot.some s)

Tactic:
mem_insert.2 <| s.eq_empty_or_nonempty.imp max_eq_bot.2 max_mem_image_coe

Premises used: Iff.mpr, Finset.max_mem_image_coe, Finset.mem_insert, Finset.max_eq_bot, Or.imp, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ s.min ∈ insert ⊤ (image WithTop.some s)

Tactic:
mem_insert.2 <| s.eq_empty_or_nonempty.imp min_eq_top.2 min_mem_image_coe

Premises used: Iff.mpr, Finset.mem_insert, Finset.min_mem_image_coe, Finset.min_eq_top, Or.imp, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max' s0 ≠ x

Tactic:
ne_of_mem_erase (max'_mem _ s0)

Premises used: Finset.max'_mem, Finset.ne_of_mem_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).min' s0 ≠ x

Tactic:
ne_of_mem_erase (min'_mem _ s0)

Premises used: Finset.min'_mem, Finset.ne_of_mem_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
pos : ∀ (s0 : (s.erase x).Nonempty), (s.erase x).max ≠ (↑x : WithBot α)
neg : ∀ (s0 : s.erase x = ∅), (s.erase x).max ≠ (↑x : WithBot α)
⊢ (s.erase x).max ≠ (↑x : WithBot α)

Tactic:
by_cases! s0 : (s.erase x).Nonempty

Premises used: Finset.Nonempty, Finset.erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ (↑x : WithBot α)

Tactic:
ne_of_eq_of_ne (coe_max' s0).symm ?_

Premises used: ne_of_eq_of_ne, Eq.symm, Finset.coe_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
pos : (↑((s.erase x).max' s0) : WithBot α) ≠ (↑x : WithBot α)
⊢ (s.erase x).max ≠ (↑x : WithBot α)

Tactic:
refine ne_of_eq_of_ne (coe_max' s0).symm ?_

Premises used: ne_of_eq_of_ne, Eq.symm, Finset.coe_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (↑((s.erase x).max' s0) : WithBot α) ≠ (↑x : WithBot α)

Tactic:
WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)

Premises used: Iff.mpr, Finset.max'_erase_ne_self, Iff.not, WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (↑((s.erase x).max' s0) : WithBot α) ≠ (↑x : WithBot α)

Tactic:
exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)

Premises used: Iff.mpr, Finset.max'_erase_ne_self, Iff.not, WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
neg : ⊥ ≠ (↑x : WithBot α)
⊢ (s.erase x).max ≠ (↑x : WithBot α)

Tactic:
rw [s0, max_empty]

Premises used: Finset.max_empty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ ⊥ ≠ (↑x : WithBot α)

Tactic:
WithBot.bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ ⊥ ≠ (↑x : WithBot α)

Tactic:
exact WithBot.bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
apply :
  ¬Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (s.erase x).min)
      (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (↑x : WithTop α))
⊢ (s.erase x).min ≠ (↑x : WithTop α)

Tactic:
apply mt (congr_arg (WithTop.map toDual))

Premises used: OrderDual.toDual, WithTop.map, mt, congr_arg, DFunLike.coe