-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_mem_of_nonempty (hs : s.Nonempty) : s.sup f ∈ f '' s

Proof state:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

Tactic:
rw [sup_eq_right.mpr ha]

Result:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ s.sup f ∈ f '' insert a ↑s

Proof state:
case empty
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : ∅.Nonempty
⊢ False

Tactic:
simp only [Finset.not_nonempty_empty] at hs

Result:
no goals

Proof state:
case insert.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
⊢ f a ⊔ s.sup f ∈ f '' ↑(insert a s)

Tactic:
simp only [Finset.coe_insert]

Result:
case insert.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

Proof state:
case empty
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : ∅.Nonempty
⊢ ∅.sup f ∈ f '' ↑∅

Tactic:
exfalso

Result:
case empty
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : ∅.Nonempty
⊢ False

Proof state:
case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ (insert a s).sup f ∈ f '' ↑(insert a s)

Tactic:
rw [Finset.sup_insert (b := a) (s := s) (f := f)]

Result:
case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ f a ⊔ s.sup f ∈ f '' ↑(insert a s)

Proof state:
case insert.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s = ∅
⊢ f a ⊔ s.sup f ∈ f '' ↑(insert a s)

Tactic:
simp [hs]

Result:
no goals

Proof state:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ s.sup f ∈ f '' insert a ↑s

Tactic:
exact Set.image_mono (Set.subset_insert a s) (h hs)

Result:
no goals

Proof state:
case insert.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

Tactic:
rcases le_total (f a) (s.sup f) with (ha | ha)

Result:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

Proof state:
case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ⊔ s.sup f ∈ f '' insert a ↑s

Tactic:
rw [sup_eq_left.mpr ha]

Result:
case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a ↑s

Proof state:
case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a ↑s

Tactic:
apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

Result:
no goals