Commit 2024-06-05 02:13 c2b953ad

View on Github →

chore(*): remove refine' (#13385) Some of these changes are simple replacements, others are more involved.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

modified def ModuleCat.ExtendRestrictScalarsAdj.Counit.map

Modified Mathlib/Algebra/Field/ULift.lean

Modified Mathlib/Algebra/Group/Aut.lean

modified def AddAut.toPerm

modified def MulAut.toPerm

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

modified def LinearMap.codRestrict

Modified Mathlib/Algebra/PUnitInstances.lean

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

modified def RingHom.id

Modified Mathlib/Algebra/Star/Subalgebra.lean

modified def StarSubalgebra.subtype

Modified Mathlib/Control/Applicative.lean

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Control/Bifunctor.lean

Modified Mathlib/Control/Traversable/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Multiset/Functor.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean