∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
        (∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (nhds 0) (nhds 0)) →
          (∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (nhds 0) (nhds 0)) →
            (∀ (x₀ : R), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) → IsTopologicalRing R