Commit 2026-02-18 18:21 6adfa6a6

chore: remove redundant Aesop imports (#35474) This PR removes redundant imports of Aesop. Two transitive imports had to be restored. These redundant imports can appear due to grind replacing aesop, and due to the new shake getting fussy about preserving public imports (I don't fully understand why shake adds these redundant imports). This helps improve parallellism when building mathlib.