-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Finite.ciSup_lt_iff {s : Set ι} {f : ι → α} (hs : s.Finite)
    (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∈ s
hx : f x = a✝
⊢ x ∈ s

Tactic:
assumption

Result:
no goals

Proof state:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
⊢ ⨆ i ∈ s, f i < a

Tactic:
have := hs.ciSup_mem_image _ h

Result:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
this : ⨆ i ∈ s, f i ∈ f '' s
⊢ ⨆ i ∈ s, f i < a

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i => ⨆ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ (range fun i => ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i => ⨆ (_ : i ∈ s), f i

Tactic:
simp only [mem_range]

Result:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = f x

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ (range fun i => ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}

Tactic:
intro

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i => ⨆ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sSup ∅}

Proof state:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
this : ∃ x ∈ s, f x = ⨆ i ∈ s, f i
⊢ ⨆ i ∈ s, f i < a

Tactic:
obtain ⟨_, hmem, hx⟩ := this

Result:
case mpr.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨆ i ∈ s, f i
⊢ ⨆ i ∈ s, f i < a

Proof state:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

Tactic:
intro h x hx

Result:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x < a

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i => ⨆ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sSup ∅}

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
  forall_exists_index]

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sSup ∅) = a✝ → a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = f x

Tactic:
refine ⟨x, ?_⟩

Result:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ⨆ (_ : x ∈ s), f x = f x

Proof state:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
intro H

Result:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
⊢ ⨆ i ∈ s, f i < a

Proof state:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x < a

Tactic:
refine h.trans_le' (le_csSup ?_ ?_)

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i => ⨆ (_ : i ∈ s), f i)

case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i => ⨆ (_ : i ∈ s), f i

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sSup ∅) = a✝ → a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
intro x hx

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
hx : (if x ∈ s then f x else sSup ∅) = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∉ s
hx : sSup ∅ = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
simp_all

Result:
no goals

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
hx : (if x ∈ s then f x else sSup ∅) = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
split_ifs at hx

Result:
case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∈ s
hx : f x = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∉ s
hx : sSup ∅ = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ⨆ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]

Result:
no goals