have : x ∈ g '' univ := by
  contrapose! hx
  rw [sb_set, mem_iUnion]
  use 0
  rw [sb_aux, mem_diff]
  sorry
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
⊢ g (invFun g x) = x
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x