chore: more cancelling pairs (#34051)

Found by the linter at #34024.

Author: adomani

Mathlib/Algebra/Ring/Units.lean

@@ -138,5 +138,3 @@ theorem isUnit_map (f : α →+* β) {a : α} : IsUnit a → IsUnit (f a) :=
 end Semiring
 
 end RingHom
-
-variable [Semiring α] [Semiring β]

Mathlib/Analysis/Normed/Order/Basic.lean

@@ -13,12 +13,3 @@ public import Mathlib.Analysis.Normed.Group.Basic
 In this file, we define classes for fields and groups that are both normed and ordered.
 These are mostly useful to avoid diamonds during type class inference.
 -/
-
-public section
-
-
-open Filter Set
-
-open Topology
-
-variable {α : Type*}

Mathlib/Data/Matrix/Basic.lean

@@ -928,8 +928,6 @@ def transposeAlgEquiv [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableE
     commutes' := fun r => by
       simp only [algebraMap_eq_diagonal, diagonal_transpose, MulOpposite.algebraMap_apply] }
 
-variable {R m α}
-
 end Transpose
 
 section NonUnitalNonAssocSemiring

Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

@@ -150,8 +150,6 @@ theorem uniformity_eq_comap_nhds_one_swapped :
   rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def]
   simp
 
-variable {Gₗ Gᵣ}
-
 end LeftRight
 
 section IsUniformGroup
@@ -412,8 +410,6 @@ theorem IsUniformGroup.uniformity_countably_generated [(𝓝 (1 : α)).IsCountab
   rw [uniformity_eq_comap_nhds_one]
   exact Filter.comap.isCountablyGenerated _ _
 
-open MulOpposite
-
 end
 
 section OfLeftAndRight