by_cases gyA : g y ∈ A
α : 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 : β
⊢ ∃ a, h a = y
case pos
α : 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 : β
gyA : g y ∈ A
⊢ ∃ a, h a = y

case neg
α : 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 : β
gyA : g y ∉ A
⊢ ∃ a, h a = y