have : x ∈ g '' univ := by
  contrapose! hx
  rw [sbSet, mem_iUnion]
  use 0
  rw [sbAux, mem_diff]
  exact ⟨mem_univ _, hx⟩
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
⊢ g (invFun g x) = x
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x