-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
    ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α)

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)

Tactic:
change _ = ite _ _ _

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) =
    if (fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s) then ⊤
    else ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))

Proof state:
case pos.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h1 : (fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤

Tactic:
cases h1 (mem_image_of_mem _ hx)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
rcases h with h1 | h2

Result:
case pos.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h1 : (fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤

case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a => ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)

Tactic:
obtain ⟨x, hx⟩ := hs

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)

Proof state:
case neg.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s))
⊢ Injective fun a => ↑a

Tactic:
exact Option.some_injective _

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) =
    if (fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s) then ⊤
    else ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s)
⊢ ↑(sInf s) = ⊤

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))

Proof state:
case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a => ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))

Tactic:
rw [preimage_image_eq]

Result:
case neg.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a => ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a => ↑a) '' s))
⊢ Injective fun a => ↑a