-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.ciSup_eq_max'_image {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x)
    (h' : (s.image f).Nonempty

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ a ∈ s, ∃ a_2, f a ≤ if a_2 ∈ s then f a_2 else sSup ∅

Tactic:
intro i hi

Result:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
hi : i ∈ s
⊢ ∃ a, f i ≤ if a ∈ s then f a else sSup ∅

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ x ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, ∃ y ∈ f '' ↑s, x ≤ y

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
  exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x

Tactic:
simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
  exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ a ∈ s, ∃ a_2, f a ≤ if a_2 ∈ s then f a_2 else sSup ∅

Proof state:
case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

Tactic:
exact ⟨_, by assumption, le_rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
rw [iSup, ← h'.csSup_eq_max', coe_image]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ s), f i) = sSup (f '' ↑s)

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
hi : i ∈ s
⊢ f i ≤ if i ∈ s then f i else sSup ∅

Tactic:
simp [hi]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∈ s
⊢ i ∈ s

Tactic:
assumption

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ s), f i) = sSup (f '' ↑s)

Tactic:
refine csSup_eq_csSup_of_forall_exists_le ?_ ?_

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ x ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, ∃ y ∈ f '' ↑s, x ≤ y

case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
hi : i ∈ s
⊢ ∃ a, f i ≤ if a ∈ s then f a else sSup ∅

Tactic:
refine ⟨i, ?_⟩

Result:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
hi : i ∈ s
⊢ f i ≤ if i ∈ s then f i else sSup ∅

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a

Tactic:
split_ifs

Result:
case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
obtain ⟨a, ha, ha'⟩ := h

Result:
case neg.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∉ s
a : ι
ha : a ∈ s
ha' : sSup ∅ ≤ f a
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
⊢ ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1

Tactic:
intro i

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : autoParam (image f s).Nonempty _auto✝
i : ι
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a

Proof state:
case neg.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h' : autoParam (image f s).Nonempty _auto✝
i : ι
h✝ : i ∉ s
a : ι
ha : a ∈ s
ha' : sSup ∅ ≤ f a
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
exact ⟨a, ha, ha'⟩

Result:
no goals