chore: import Aesop.Frontend when declaring aesop rule sets (leanprover-community#35165)

This PR turns some `import Aesop` into `import Aesop.Frontend` in places where we want to tag `aesop` lemmas, but do not yet want to use the tactic itself.

Author: JovanGerb

Mathlib/Data/Finset/Attr.lean

@@ -6,8 +6,7 @@ Authors: Yaël Dillies
 module
 
 public import Mathlib.Init
-public import Aesop
-public import Aesop.Frontend.Basic
+public import Aesop.Frontend
 
 /-!
 # Aesop rule set for finsets

Mathlib/Data/Prod/Lex.lean

@@ -73,7 +73,7 @@ instance [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedRela
 instance instPreorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β) where
   le_refl := refl_of <| Prod.Lex _ _
   le_trans _ _ _ := trans_of <| Prod.Lex _ _
-  lt_iff_le_not_ge x₁ x₂ := by aesop (add simp [le_iff, lt_iff, lt_iff_le_not_ge])
+  lt_iff_le_not_ge x₁ x₂ := by grind [le_iff, lt_iff, lt_iff_le_not_ge]
 
 /-- See also `monotone_fst_ofLex` for a version stated in terms of `Monotone`. -/
 theorem monotone_fst [Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) :

Mathlib/Tactic/Finiteness/Attr.lean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 module
 
 public import Mathlib.Init
-public import Aesop
+public import Aesop.Frontend
 
 /-! # Finiteness tactic attribute -/
 

Mathlib/Tactic/SetLike.lean

@@ -5,10 +5,9 @@ Authors: Jireh Loreaux
 -/
 module
 
-public import Aesop
+public import Aesop.Frontend
 public meta import Batteries.Util.LibraryNote
 public import Mathlib.Tactic.Basic
-public import Aesop.Frontend.Basic
 
 /-!
 # SetLike Rule Set