have : x ∈ A := by
  rw [A_def, sbSet, mem_iUnion]
  exact ⟨n, xmem⟩
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ h x = y
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y