chore: remove superfluous opens (leanprover-community#38462)

or downgrade them to `open scoped`.
In particular, many `open Pointwise` can become `open scoped Pointwise`;
probably they became bare `open` during mathport. Not exhaustive.

Author: grunweg

Archive/Imo/Imo1962Q4.lean

@@ -16,8 +16,6 @@ in fact the simplest form of the set of solutions, and then prove it equals the
 
 open Real
 
-open scoped Real
-
 namespace Imo1962Q4
 
 noncomputable section

Archive/Imo/Imo1987Q1.lean

@@ -29,8 +29,6 @@ open Equiv Fintype Function
 
 open Finset (range sum_const)
 
-open Set (Iic)
-
 namespace Imo1987Q1
 
 /-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs

Archive/Imo/Imo2019Q2.lean

@@ -58,9 +58,7 @@ rather than more literally with `affineSegment`.
 
 
 open Affine Affine.Simplex EuclideanGeometry Module
-
-open scoped Affine EuclideanGeometry Real
-
+open scoped Real
 
 attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 

Counterexamples/MapFloor.lean

@@ -42,8 +42,6 @@ noncomputable section
 
 open Function Int Polynomial
 
-open scoped Polynomial
-
 /-- The integers with infinitesimals adjoined. -/
 def IntWithEpsilon :=
   ℤ[X] deriving Nontrivial, CommRing, Inhabited

Counterexamples/SeminormLatticeNotDistrib.lean

@@ -18,7 +18,6 @@ This proves the lattice `Seminorm ℝ (ℝ × ℝ)` is not distributive.
 * https://en.wikipedia.org/wiki/Seminorm#Examples
 -/
 
-
 open Seminorm
 
 open scoped NNReal

Counterexamples/SorgenfreyLine.lean

@@ -34,8 +34,7 @@ Prove that the Sorgenfrey line is a paracompact space.
 
 
 open Set Filter TopologicalSpace
-
-open scoped Topology Filter Cardinal
+open scoped Topology Cardinal
 
 namespace Counterexample
 

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -42,7 +42,6 @@ This theory will serve as the foundation for spectral theory in Banach algebras.
 
 @[expose] public section
 
-
 open Set
 
 open scoped Pointwise Ring

Mathlib/Algebra/Category/Grp/Biproducts.lean

@@ -17,10 +17,7 @@ public import Mathlib.Tactic.CategoryTheory.Elementwise
 
 @[expose] public section
 
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits
 
 universe w u
 

Mathlib/Algebra/Category/Grp/Images.lean

@@ -17,16 +17,12 @@ from the fact that `AddCommGrpCat` is an abelian category.
 
 @[expose] public section
 
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits
 
 universe u
 
 namespace AddCommGrpCat
 
-
 -- Note that because `injective_of_mono` is currently only proved in `Type 0`,
 -- we restrict to the lowest universe here for now.
 variable {G H : AddCommGrpCat.{0}} (f : G ⟶ H)

Mathlib/Algebra/Category/Grp/Injective.lean

@@ -28,8 +28,6 @@ in `Mathlib/Algebra/Category/Grp/EnoughInjectives.lean`.
 
 open CategoryTheory
 
-open Pointwise
-
 universe u
 
 variable (A : Type u) [AddCommGroup A]