∀ {α : Type u_2} {β : Type u_1} {f : α → β} (hf : Function.Surjective f),
  (∀ (b : β), f (Function.surjInv hf b) = b) →
    ∀ (x : α),
      (∀ x_1 ∉ Set.range (Function.surjInv hf), x_1 ∈ {x}) →
        ∀ (a b : α),
          a ∈ Set.range (Function.surjInv hf) →
            b ∉ Set.range (Function.surjInv hf) → f a = f b → ¬a = b → a = x ∨ a = Function.surjInv hf (f x)