case intro
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
hs : Set.Nonempty s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)
obtain ⟨x, hx⟩ := hs
case intro
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
⊢ ↑(sInf s) = if (fun a => ↑a) '' s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
case intro
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a => ↑a) '' s)
change _ = ite _ _ _
case intro.inl
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : (fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤

case intro.inr
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : ¬(fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
case intro
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
⊢ ↑(sInf s) = if (fun a => ↑a) '' s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
split_ifs with h
no goals
case intro.inl
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : (fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤
cases h (mem_image_of_mem _ hx)
case intro.inr.h
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : ¬(fun a => ↑a) '' s ⊆ {⊤}
⊢ Injective fun a => ↑a
case intro.inr
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : ¬(fun a => ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
rw [preimage_image_eq]
no goals
case intro.inr.h
α : Type u_1
β : Type ?u.2948
γ : Type ?u.2951
ι : Sort ?u.2954
inst✝ : InfSet α
s : Set α
x : α
hx : x ∈ s
h : ¬(fun a => ↑a) '' s ⊆ {⊤}
⊢ Injective fun a => ↑a
exact Option.some_injective _