∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X]
  (motive :
    (ContinuousSMul G X ∧
        ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
          Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
            ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)) →
      Prop)
  (x :
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
          ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)),
  (∀ (cont : ContinuousSMul G X)
      (h :
        ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
          Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
            ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)),
      motive ⋯) →
    motive x