chore: revert module keyword on incompatible Archive files

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Archive/Examples/IfNormalization/Result.lean

@@ -1,15 +1,11 @@
-module
 /-
 Copyright (c) 2023 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-public import Archive.Examples.IfNormalization.Statement
-public import Mathlib.Data.List.AList
-public import Mathlib.Tactic.Recall
-
-
-@[expose] public section
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
+import Mathlib.Tactic.Recall
 
 /-!
 # A solution to the if normalization challenge in Lean.

Archive/Examples/IfNormalization/Statement.lean

@@ -1,12 +1,9 @@
-module
 /-
 Copyright (c) 2023 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-@[expose] public section
-
 /-!
 # If normalization
 

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -1,14 +1,10 @@
-module
 /-
 Copyright (c) 2023 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Kim Morrison
 -/
-public import Archive.Examples.IfNormalization.Statement
-public import Mathlib.Data.List.AList
-
-
-@[expose] public section
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
 
 /-!
 # A variant of Chris Hughes' solution for the if normalization challenge.

Archive/Examples/MersennePrimes.lean

@@ -1,13 +1,9 @@
-module
 /-
 Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-public import Mathlib.NumberTheory.LucasLehmer
-
-
-@[expose] public section
+import Mathlib.NumberTheory.LucasLehmer
 
 /-!
 # Explicit Mersenne primes

Archive/Imo/Imo1982Q3.lean

@@ -1,14 +1,10 @@
-module
 /-
 Copyright (c) 2024 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios, Alex Brodbelt
 -/
-public import Mathlib.Algebra.Order.Field.GeomSum
-public import Mathlib.Data.NNReal.Basic
-
-
-@[expose] public section
+import Mathlib.Algebra.Order.Field.GeomSum
+import Mathlib.Data.NNReal.Basic
 
 /-!
 # IMO 1982 Q3

Archive/Imo/Imo2024Q1.lean

@@ -1,19 +1,15 @@
-module
 /-
 Copyright (c) 2024 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-public import Mathlib.Algebra.BigOperators.Intervals
-public import Mathlib.Algebra.BigOperators.Ring.Finset
-public import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
-public import Mathlib.Algebra.Order.ToIntervalMod
-public import Mathlib.Data.Real.Archimedean
-public import Mathlib.Tactic.Peel
-public import Mathlib.Tactic.Recall
-
-
-@[expose] public section
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
+import Mathlib.Algebra.Order.ToIntervalMod
+import Mathlib.Data.Real.Archimedean
+import Mathlib.Tactic.Peel
+import Mathlib.Tactic.Recall
 
 /-!
 # IMO 2024 Q1

Archive/Imo/Imo2024Q5.lean

@@ -1,19 +1,15 @@
-module
 /-
 Copyright (c) 2024 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-public import Mathlib.Data.Fin.VecNotation
-public import Mathlib.Data.List.ChainOfFn
-public import Mathlib.Data.List.TakeWhile
-public import Mathlib.Data.Nat.Dist
-public import Mathlib.Data.Fintype.Fin
-public import Mathlib.Tactic.IntervalCases
-public import Mathlib.Tactic.FinCases
-
-
-@[expose] public section
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Data.List.ChainOfFn
+import Mathlib.Data.List.TakeWhile
+import Mathlib.Data.Nat.Dist
+import Mathlib.Data.Fintype.Fin
+import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.FinCases
 
 /-!
 # IMO 2024 Q5

Archive/MiuLanguage/DecisionNec.lean

@@ -1,15 +1,11 @@
-module
 /-
 Copyright (c) 2020 Gihan Marasingha. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gihan Marasingha
 -/
-public import Archive.MiuLanguage.Basic
-public import Mathlib.Data.List.Basic
-public import Mathlib.Data.Nat.ModEq
-
-
-@[expose] public section
+import Archive.MiuLanguage.Basic
+import Mathlib.Data.List.Basic
+import Mathlib.Data.Nat.ModEq
 
 /-!
 # Decision procedure: necessary condition