have x₁A : x₁ ∈ A := by
  apply not_imp_self.mp
  intro x₁nA
  rw [if_pos xA, if_neg x₁nA] at hxeq
  rw [A_def, sb_set, mem_iUnion] at xA
  have x₁eq : x₁ = g (f x₂) := by
    rw [← sb_right_inv f g x₁nA, hxeq]
  rcases xA with ⟨n, hn⟩
  rw [A_def, sb_set, mem_iUnion]
  use n + 1
  simp [sb_aux]
  exact ⟨x₂, hn, x₁eq.symm⟩
case pos.inr
α✝ : 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 : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₂ ∈ A
⊢ x₁ = x₂
case pos.inr
α✝ : 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 : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₁ = x₂