{R : Type u_1} →
  [inst : TopologicalSpace R] →
    {A : Type u_2} →
      [inst_1 : Add A] →
        [inst_2 : SMul R A] →
          [τA : TopologicalSpace A] →
            {motive : IsModuleTopology R A → Sort u} →
              ((eq_moduleTopology' : τA = moduleTopology R A) → motive ⋯) → (t : IsModuleTopology R A) → motive t