-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_maximal_wrt [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite)
    (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Proof state:
case neg
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
refine ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => ?_⟩

Result:
case neg
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
⊢ f b = f c

Proof state:
case empty
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s : Set α
hs : ∅.Nonempty
⊢ ∃ a ∈ ∅, ∀ a' ∈ ∅, f a ≤ f a' → f a = f a'

Tactic:
exact absurd hs not_nonempty_empty

Result:
no goals

Proof state:
case neg.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
c : α
hbc : f b ≤ f c
his : c ∉ s
hs : (insert c s).Nonempty
h : ¬f b ≤ f c
hc : c ∈ insert c s
⊢ f b = f c

Tactic:
exact (h hbc).elim

Result:
no goals

Proof state:
case pos
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
refine ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac ?_⟩

Result:
case pos
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
⊢ f c ≤ f a

Proof state:
case insert
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Result:
case insert.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s = ∅
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

case insert.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s.Nonempty
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Proof state:
case pos
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
⊢ f c ≤ f a

Tactic:
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)

Result:
case pos.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
c : α
his : c ∉ s
hs : (insert c s).Nonempty
h : f b ≤ f c
hc : c ∈ insert c s
hac : f c ≤ f c
⊢ f c ≤ f c

case pos.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
hcs : c ∈ s
⊢ f c ≤ f a

Proof state:
case insert.inr.intro.intro
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
by_cases h : f b ≤ f a

Result:
case pos
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

case neg
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Proof state:
case pos.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
hcs : c ∈ s
⊢ f c ≤ f a

Tactic:
rwa [← ih c hcs (le_trans h hac)]

Result:
no goals

Proof state:
case insert.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s = ∅
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
use a

Result:
case h
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s = ∅
⊢ a ∈ insert a s ∧ ∀ a' ∈ insert a s, f a ≤ f a' → f a = f a'

Proof state:
case neg.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
hcs : c ∈ s
⊢ f b = f c

Tactic:
exact ih c hcs hbc

Result:
no goals