rw [A_def, sb_set, mem_iUnion]
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ x₁ ∈ A
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ ∃ i, x₁ ∈ sb_aux f g i