Commit 2025-08-07 16:22 b1407cb3

View on Github →

chore: replace aesop with simp where applicable (#28018)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/CategoryTheory/Products/Basic.lean

modified theorem CategoryTheory.Prod.fac'

modified theorem CategoryTheory.Prod.fac

Modified Mathlib/CategoryTheory/Subpresheaf/Image.lean

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Order/IsLUB.lean

Modified Mathlib/Topology/Sets/Opens.lean

Modified Mathlib/Topology/Spectral/Prespectral.lean