Commit 2024-08-19 13:15 9e23bfc0

View on Github →

chore: replace last uses of lambda instead of fun (#15973) Split out from #15896.

Estimated changes

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Lean/Meta/CongrTheorems.lean

Modified Mathlib/Order/Filter/NAry.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

Modified Mathlib/Tactic/FunProp/ToBatteries.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/Simps/NotationClass.lean

modified def Simps.copyFirst

modified def Simps.copySecond

modified def Simps.defaultfindArgs

modified def Simps.findCoercionArgs

modified def Simps.findOneArgs

modified def Simps.findZeroArgs

modified def Simps.nsmulArgs

modified def Simps.zsmulArgs