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

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

Tactic:
simp only [mem_image] at this

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

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

Tactic:
refine h.trans_le (csInf_le ?_ ?_)

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow (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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i => ⨅ (_ : i ∈ s), f i

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

Tactic:
constructor

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

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

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

Tactic:
exact H _ hmem

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, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i

Tactic:
intro H

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

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

Tactic:
exact Or.inr ⟨_, by assumption, hx⟩

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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow (range fun i => ⨅ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow

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

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
hx : (if x ∈ s then f x else sInf ∅) = a✝
⊢ a✝ = sInf ∅ ∨ ∃ 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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∈ s
hx : f x = a✝
⊢ a✝ = sInf ∅ ∨ ∃ 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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∉ s
hx : sInf ∅ = a✝
⊢ a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝

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

Tactic:
rw [← hx]

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

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

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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ a < f x

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

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, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨅ i ∈ s, f i
⊢ a < ⨅ i ∈ s, f i

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

Tactic:
have := hs.ciInf_mem_image _ h

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

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ⨅ (_ : x ∈ s), f x = f x

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

Tactic:
assumption

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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ (range fun i => ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}

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, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i => ⨅ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sInf ∅}