more tidying up

Author: kbuzzard

FLT/ForMathlib/module_topology.lean

@@ -520,8 +520,6 @@ def Module.topologicalRing : TopologicalRing D :=
 
 end commutative
 
-set_option linter.unusedTactic false
-
 lemma continuousSMul (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
     (A : Type*) [AddCommGroup A] [Module R A] [Module.Finite R A] [TopologicalSpace A]
     [IsModuleTopology R A] :
@@ -536,8 +534,7 @@ end ModuleTopology
 
 I can only prove that `SMul : R × A → A` is continuous for the module topology if `R` is
 commutative (because my proof uses tensor products) and if `A` is finite (because
-I reduce to a basis check ). Is it true in general
-
+I reduce to a basis check ). Is it true in general?
 
 lemma continuousSMul (R : Type*) [Ring R] [TopologicalSpace R] [TopologicalRing R]
     (A : Type*) [AddCommGroup A] [Module R A] : @ContinuousSMul R A _ _ (moduleTopology R A) := by
@@ -546,6 +543,4 @@ lemma continuousSMul (R : Type*) [Ring R] [TopologicalSpace R] [TopologicalRing
   rw [isModuleTopology R R]
   refine Module.continuous_bilinear ?_
   sorry
-  done
-end ModuleTopology
 -/