use n + 1
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ i, x₂ ∈ sbAux f g i
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ sbAux f g (n + 1)