awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
rw :
  ¬Eq (α := WithTop αᵒᵈ)
      (Finset.max (erase (image (⇑toDual : (a : α) → αᵒᵈ) s) ((toDual : (a : α) → αᵒᵈ) x)) : WithBot αᵒᵈ)
      ((↑((toDual : (a : α) → αᵒᵈ) x) : WithTop αᵒᵈ) : WithTop αᵒᵈ)
⊢ ¬Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (s.erase x).min)
      (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (↑x : WithTop α))

Tactic:
rw [map_toDual_min, image_erase toDual.injective, WithTop.map_coe]

Premises used: OrderDual.toDual, Finset.map_toDual_min, Equiv.injective, Finset.image_erase, WithTop.map_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
⊢ ¬Eq (α := WithTop αᵒᵈ)
      (Finset.max (erase (image (⇑toDual : (a : α) → αᵒᵈ) s) ((toDual : (a : α) → αᵒᵈ) x)) : WithBot αᵒᵈ)
      ((↑((toDual : (a : α) → αᵒᵈ) x) : WithTop αᵒᵈ) : WithTop αᵒᵈ)

Tactic:
apply max_erase_ne_self

Premises used: Finset.max_erase_ne_self
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ x < y

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
⊢ x < {x_1 ∈ s | x < x_1}.min' Hne

Tactic:
simp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
z : α
hzs : z ∈ s
hz : x < z
⊢ x < z

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, y < x
⊢ ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y

Tactic:
@exists_next_right αᵒᵈ _ x s h

Premises used: Set.Mem, setOf, Finset.exists_next_right, OrderDual
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
rcases : ∀ (a : α) (has : a ∈ s) (hxa : x < a) (ha : ∀ z ∈ s, x < z → a ≤ z), ∃ z ∈ t, x < z ∧ z < y
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩

Premises used: Finset.exists_next_right, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ z ∈ s, x < z → a ≤ z
rcases : ∀ (b : α) (hbt : b ∈ t) (hxb : x < b) (hba : b < a), ∃ z ∈ t, x < z ∧ z < y
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩

Premises used: And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ z ∈ s, x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ z ∈ s, x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
hxy : x < y
rcases : ∀ (a : α) (hat : a ∈ t) (hxa : x < a) (hay : a < y), f x < f y
⊢ f x < f y

Tactic:
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ {y_1 ∈ t | y < y_1}
⊢ y < b

Tactic:
simpa using (mem_filter.1 hb).2

Premises used: And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y

Tactic:
calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)

Premises used: Iff.mpr, WithTop.coe_lt_top, Finset.min_le, Finset.lt_inf_iff, WithTop.coe_lt_coe, And.intro, LT.lt.trans, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
⊢ StrictMonoOn f (↑s : Set α)

Tactic:
have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f (↑s : Set α)
⊢ #s = #(image f s)

Tactic:
(card_image_of_injOn f_mono.injOn).symm

Premises used: StrictMonoOn.injOn, Finset.card_image_of_injOn, Eq.symm
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f (↑s : Set α)
⊢ #(image f s) ≤ #(insert ⊤ (image WithTop.some t))

Tactic:
card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)

Premises used: Iff.mpr, Finset.insert_subset_insert, Finset.filter_subset, Finset.image_subset_iff, Finset.image_subset_image, LT.lt, Top.top, Finset.filter, Finset.card_mono, Finset.min_mem_insert_top_image_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f (↑s : Set α)
⊢ #(insert ⊤ (image WithTop.some t)) ≤ #t + 1

Tactic:
(card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

Premises used: Nat.add_le_add_right, Finset.card_insert_le, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f (↑s : Set α)
⊢ #s ≤ #t + 1

Tactic:
calc
    s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

Premises used: Iff.mpr, StrictMonoOn.injOn, Finset.insert_subset_insert, Nat.add_le_add_right, Finset.filter_subset, Insert.insert, Finset.card_insert_le, Finset.card_image_le, Finset.image_subset_iff, Finset.image_subset_image, Finset.card, Finset.card_image_of_injOn, LE.le.trans, Top.top, Eq.symm, Finset.filter, Finset.image, Finset.card_mono, Finset.min_mem_insert_top_image_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #(t \ s) + 1

Tactic:
card_le_of_interleaved fun x hx y hy hxy hs =>
    let ⟨z, hzt, hxz, hzy⟩ := h x hx y hy hxy hs
    ⟨z, mem_sdiff.2 ⟨hzt, fun hzs => hs z hzs ⟨hxz, hzy⟩⟩, hxz, hzy⟩

Premises used: Iff.mpr, Membership.mem, Exists, Finset.mem_sdiff, SDiff.sdiff, And, Finset.card_le_of_interleaved, And.intro, LT.lt, _private.0.Finset.card_le_diff_of_interleaved.match_1, Exists.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
H : ∀ (s : Finset α) (ih : ∀ s_1 ∈ s, motive (s.erase s_1)), motive s
⊢ motive s

Tactic:
induction s using Finset.eraseInduction with | _ s ih

Premises used: Finset.eraseInduction
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
H : ∀ (ih : ∀ (s : α), Membership.mem (γ := Finset α) ∅ s → motive (erase ∅ s)), motive ∅
H₁ : ∀ (hne : s.Nonempty), motive s
⊢ motive s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ (s : α), Membership.mem (γ := Finset α) ∅ s → motive (erase ∅ s)
⊢ motive ∅

Tactic:
empty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ (s : α), Membership.mem (γ := Finset α) ∅ s → motive (erase ∅ s)
⊢ motive ∅

Tactic:
exact empty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : ∀ (H : s.max' hne ∈ s), motive s
⊢ motive s

Tactic:
have H : s.max' hne ∈ s := max'_mem s hne
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
H₁ : motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))
⊢ motive s

Tactic:
rw [← insert_erase H]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))

Tactic:
insert _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

Premises used: Finset.lt_max'_of_mem_erase_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))

Tactic:
exact insert _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

Premises used: Finset.lt_max'_of_mem_erase_max'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
@induction_on_max αᵒᵈ _ _ _ s empty insert

Premises used: Finset.induction_on_max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
H : ∀ (s : Finset ι) (ihs : ∀ s_1 ∈ s, motive (s.erase s_1)), motive s
⊢ motive s

Tactic:
induction s using Finset.eraseInduction with | _ s ihs

Premises used: Finset.eraseInduction
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
H : ∀ (hne : image f s = ∅), motive s
H₁ : ∀ (hne : (image f s).Nonempty), motive s
⊢ motive s

Tactic:
rcases (s.image f).eq_empty_or_nonempty with (hne | hne)

Premises used: Finset.image, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : image f s = ∅
⊢ s = ∅

Tactic:
simp only [image_eq_empty] at hne

Premises used: Finset.image_eq_empty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s = ∅
⊢ motive s

Tactic:
simp only [hne, empty]
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : ∀ (H : (image f s).max' hne ∈ image f s), motive s
⊢ motive s

Tactic:
have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : (image f s).max' hne ∈ image f s
⊢ ∃ a ∈ s, f a = (image f s).max' hne

Tactic:
simp only [mem_image] at H

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : ∃ a ∈ s, f a = (image f s).max' hne
H₁ : ∀ (a : ι) (has : a ∈ s) (hfa : f a = (image f s).max' hne), motive s
⊢ motive s

Tactic:
rcases H with ⟨a, has, hfa⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
H : motive (Insert.insert a (s.erase a))
⊢ motive s

Tactic:
rw [← insert_erase has]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive (Insert.insert a (s.erase a))

Tactic:
insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)

Premises used: Finset.notMem_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
H : ∀ (x : ι) (hx : x ∈ s.erase a), f x ≤ f a
⊢ motive (Insert.insert a (s.erase a))

Tactic:
refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)

Premises used: Finset.notMem_erase
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
H : f x ≤ (image f s).max' hne
⊢ f x ≤ f a

Tactic:
rw [hfa]
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ (image f s).max' hne

Tactic:
le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

Premises used: Finset.le_max', Finset.mem_of_mem_erase, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ (image f s).max' hne

Tactic:
exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

Premises used: Finset.le_max', Finset.mem_of_mem_erase, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
@induction_on_max_value αᵒᵈ ι _ _ _ _ s empty insert

Premises used: Finset.induction_on_max_value
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
obtain : ∀ (y : α) (hy : (image f s).max = (↑y : WithBot α)), ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)

Premises used: Finset.Nonempty.image, Finset.max_of_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
y : α
hy : (image f s).max = (↑y : WithBot α)
rcases : ∀ (x : β) (hx : x ∈ s) (hy : (image f s).max = (↑(f x) : WithBot α)), ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩

Premises used: Finset.mem_image, Finset.mem_of_max, Iff.mp, rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
x : β
hx : x ∈ s
hy : (image f s).max = (↑(f x) : WithBot α)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩

Premises used: Finset.le_max_of_eq, And.intro, Exists.intro, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
x : β
hx : x ∈ s
hy : (image f s).max = (↑(f x) : WithBot α)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'

Tactic:
@exists_max_image αᵒᵈ β _ s f h

Premises used: Finset.exists_max_image
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s : Set α) i ↔ IsLeast (↑s : Set α) i

Tactic:
⟨fun his => ?_, IsLeast.isGLB⟩

Premises used: IsLeast.isGLB, Iff.intro
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
refine : ∀ (his : IsGLB (↑s : Set α) i), IsLeast (↑s : Set α) i
⊢ IsGLB (↑s : Set α) i ↔ IsLeast (↑s : Set α) i

Tactic:
refine ⟨fun his => ?_, IsLeast.isGLB⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
this : i = s.min' hs
rw : IsLeast (↑s : Set α) (s.min' hs)
⊢ IsLeast (↑s : Set α) i

Tactic:
rw [this]
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
this : i = s.min' hs
⊢ IsLeast (↑s : Set α) (s.min' hs)

Tactic:
isLeast_min' s hs

Premises used: Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
this : i = s.min' hs
⊢ IsLeast (↑s : Set α) (s.min' hs)

Tactic:
exact isLeast_min' s hs

Premises used: Finset.isLeast_min'
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
suffices : i = s.min' hs
⊢ IsLeast (↑s : Set α) i

Tactic:
suffices i = min' s hs by
    rw [this]
    exact isLeast_min' s hs
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
⊢ (∀ x ∈ (↑s : Set α), i ≤ x) ∧ ∀ x ∈ lowerBounds (↑s : Set α), x ≤ i

Tactic:
rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his

Premises used: mem_lowerBounds, IsGreatest, IsGLB, mem_upperBounds