Commit 2025-11-18 15:06 5e1991c2

View on Github →

style: remove redundant <| and |>. (#31769) This PR replaces all occurrences of <| do by do, and all occurrences of (· |>. with (·..

Estimated changes

Modified Mathlib/Algebra/BigOperators/Expect.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

modified def CategoryTheory.exp.delabFunctorObjExp

Modified Mathlib/Lean/ContextInfo.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

modified def Mathlib.Tactic.Borelize.borelize

Modified Mathlib/Tactic/ApplyFun.lean

Modified Mathlib/Tactic/HigherOrder.lean

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

modified def Mathlib.Meta.NormNum.deriveNotPrime

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/TacticAnalysis.lean

Modified Mathlib/Tactic/Translate/Core.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Util/AddRelatedDecl.lean

Modified Mathlib/Util/WhatsNew.lean

Modified MathlibTest/Expr.lean

Modified MathlibTest/Simps.lean

Modified MathlibTest/random.lean