∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X)
  (motive : (∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f) → Prop)
  (x_1 : ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f),
  (∀ (g : Y → X) (hgc : ContinuousAt g (f x)) (hgx : g (f x) = x) (hgf : Function.RightInverse g f), motive ⋯) →
    motive x_1