chore: remove unused sections in front of lone declare_aesop_rule_sets

Author: thorimur

Mathlib/Combinatorics/Matroid/Init.lean

@@ -16,6 +16,4 @@ This module defines the `Matroid` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [Matroid]

Mathlib/Combinatorics/SimpleGraph/Init.lean

@@ -16,6 +16,4 @@ This module defines the `SimpleGraph` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [SimpleGraph]

Mathlib/Data/Finset/Attr.lean

@@ -14,8 +14,6 @@ public import Aesop.Frontend
 This file defines `finsetNonempty`, an aesop rule set to prove that a given finset is nonempty.
 -/
 
-public section
-
 -- `finsetNonempty` rules try to prove that a given finset is nonempty,
 -- for use in positivity extensions.
 declare_aesop_rule_sets [finsetNonempty] (default := true)

Mathlib/Data/Sym/Sym2/Init.lean

@@ -16,6 +16,4 @@ visible once the file in which they're declared is imported, so we must put this
 declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [Sym2]

Mathlib/Tactic/ArithMult/Init.lean

@@ -16,6 +16,4 @@ This module defines the `IsMultiplicative` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [IsMultiplicative]

Mathlib/Tactic/Bound/Init.lean

@@ -16,6 +16,4 @@ This module defines the `Bound` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Bound]

Mathlib/Tactic/Continuity/Init.lean

@@ -16,6 +16,4 @@ This module defines the `Continuous` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Continuous]

Mathlib/Tactic/Finiteness/Attr.lean

@@ -10,6 +10,4 @@ public import Aesop.Frontend
 
 /-! # Finiteness tactic attribute -/
 
-public meta section
-
 declare_aesop_rule_sets [finiteness]

Mathlib/Tactic/Measurability/Init.lean

@@ -16,6 +16,4 @@ This module defines the `Measurable` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Measurable]

Mathlib/Topology/Sheaves/Init.lean

@@ -16,7 +16,5 @@ visible once the file in which they're declared is imported, so we must put this
 declaration into its own file.
 -/
 
-public section
-
 /- to prove subset relations -/
 declare_aesop_rule_sets [Restrict]