∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : Monoid N] {f : M →* N} (U : Set (M × Mᵐᵒᵖ)) (y : Nˣ)
  (motive :
    (∃ a a_1,
        (a, MulOpposite.op a_1) ∈ U ∧
          f a = ↑y ∧
            (⇑MulOpposite.opHomeomorph ∘ ⇑f ∘ ⇑MulOpposite.opHomeomorph.symm) (MulOpposite.op a_1) =
              MulOpposite.op ↑y⁻¹) →
      Prop)
  (x :
    ∃ a a_1,
      (a, MulOpposite.op a_1) ∈ U ∧
        f a = ↑y ∧
          (⇑MulOpposite.opHomeomorph ∘ ⇑f ∘ ⇑MulOpposite.opHomeomorph.symm) (MulOpposite.op a_1) = MulOpposite.op ↑y⁻¹),
  (∀ (a b : M) (h : (a, MulOpposite.op b) ∈ U) (ha : f a = ↑y)
      (hb : (⇑MulOpposite.opHomeomorph ∘ ⇑f ∘ ⇑MulOpposite.opHomeomorph.symm) (MulOpposite.op b) = MulOpposite.op ↑y⁻¹),
      motive ⋯) →
    motive x