style: remove redundant <| and |>. (#31769)

This PR replaces all occurrences of `<| do` by `do`, and all occurrences of `(· |>.` with `(·.`.

Author: JovanGerb

Mathlib/Algebra/BigOperators/Expect.lean

@@ -86,7 +86,7 @@ open Batteries.ExtendedBinder
 /-- Delaborator for `Finset.expect`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the expect is over `Finset.univ`. -/
 @[scoped app_delab Finset.expect] def delabFinsetExpect : Delab :=
-  whenPPOption getPPNotation <| withOverApp 6 <| do
+  whenPPOption getPPNotation <| withOverApp 6 do
   let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
   let ppDomain ← getPPOption getPPFunBinderTypes

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

@@ -258,7 +258,7 @@ private def delabFinsetArg (i : Ident) : DelabM FinsetResult := do
 /-- Delaborator for `Finset.prod`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the product is over `Finset.univ`. -/
 @[app_delab Finset.prod] def delabFinsetProd : Delab :=
-  whenPPOption getPPNotation <| withOverApp 5 <| do
+  whenPPOption getPPNotation <| withOverApp 5 do
   let #[_, _, _, _, f] := (← getExpr).getAppArgs | failure
   guard f.isLambda
   let ppDomain ← getPPOption getPPFunBinderTypes
@@ -289,7 +289,7 @@ to show the domain type when the product is over `Finset.univ`. -/
 /-- Delaborator for `Finset.sum`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the sum is over `Finset.univ`. -/
 @[app_delab Finset.sum] def delabFinsetSum : Delab :=
-  whenPPOption getPPNotation <| withOverApp 5 <| do
+  whenPPOption getPPNotation <| withOverApp 5 do
   let #[_, _, _, _, f] := (← getExpr).getAppArgs | failure
   guard f.isLambda
   let ppDomain ← getPPOption getPPFunBinderTypes

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -99,7 +99,7 @@ notation:20 A " ⟹ " B:19 => (exp A).obj B
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Delaborator for `Functor.obj` -/
 @[app_delab Functor.obj]
-def delabFunctorObjExp : Delab := whenPPOption getPPNotation <| withOverApp 6 <| do
+def delabFunctorObjExp : Delab := whenPPOption getPPNotation <| withOverApp 6 do
   let e ← getExpr
   guard <| e.isAppOfArity' ``Functor.obj 6
   let A ← withNaryArg 4 do

Mathlib/Lean/ContextInfo.lean

@@ -72,7 +72,7 @@ def runTactic (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (x : MVarId 
     panic!"ContextInfo.runTactic: `goal` must be an element of `i.goalsBefore`"
   let mctx := i.mctxBefore
   let lctx := (mctx.decls.find! goal).2
-  ctx.runMetaMWithMessages lctx <| do
+  ctx.runMetaMWithMessages lctx do
     -- Make a fresh metavariable because the original goal is already assigned.
     let type ← goal.getType
     let goal ← Meta.mkFreshExprSyntheticOpaqueMVar type

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -157,7 +157,7 @@ def borelToRefl (e : Expr) (i : FVarId) : TacticM Unit := do
 /-- Given a type `$t`, if there is an assumption `[i : MeasurableSpace $t]`, then try to prove
 `[BorelSpace $t]` and replace `i` with `borel $t`. Otherwise, add instances
 `borel $t : MeasurableSpace $t` and `⟨rfl⟩ : BorelSpace $t`. -/
-def borelize (t : Term) : TacticM Unit := withMainContext <| do
+def borelize (t : Term) : TacticM Unit := withMainContext do
   let u ← mkFreshLevelMVar
   let e ← withoutRecover <| Tactic.elabTermEnsuringType t (mkSort (mkLevelSucc u))
   let i? ← findLocalDeclWithType? (← mkAppOptM ``MeasurableSpace #[e])

Mathlib/Tactic/ApplyFun.lean

@@ -31,7 +31,7 @@ def applyFunHyp (f : Term) (using? : Option Term) (h : FVarId) (g : MVarId) :
     | (``Eq, #[_, lhs, rhs]) => do
       let (eq', gs) ←
         withCollectingNewGoalsFrom (parentTag := ← g.getTag) (tagSuffix := `apply_fun) <|
-        withoutRecover <| runTermElab <| do
+        withoutRecover <| runTermElab do
           let f ← Term.elabTerm f none
           let lhs' ← Term.elabAppArgs f #[] #[.expr lhs] none false false
           let rhs' ← Term.elabAppArgs f #[] #[.expr rhs] none false false

Mathlib/Tactic/HigherOrder.lean

@@ -73,7 +73,7 @@ def higherOrderGetParam (thm : Name) (stx : Syntax) : AttrM Name := do
         updatePrefix sname.getId thm.getPrefix
       else
         thm.appendAfter "\'"
-    MetaM.run' <| TermElabM.run' <| do
+    MetaM.run' <| TermElabM.run' do
       let lvl := (← getConstInfo thm).levelParams
       let typ ← instantiateMVars (← inferType <| .const thm (lvl.map mkLevelParam))
       let hot ← mkHigherOrderType typ

Mathlib/Tactic/Linarith/Preprocessing.lean

@@ -100,7 +100,7 @@ open Zify
 `isNatProp tp` is true iff `tp` is an inequality or equality between natural numbers
 or the negation thereof.
 -/
-partial def isNatProp (e : Expr) : MetaM Bool := succeeds <| do
+partial def isNatProp (e : Expr) : MetaM Bool := succeeds do
   let (_, _, .const ``Nat [], _, _) ← e.ineqOrNotIneq? | failure
 
 /-- If `e` is of the form `((n : ℕ) : C)`, `isNatCoe e` returns `⟨n, C⟩`. -/
@@ -162,7 +162,7 @@ def natToInt : GlobalBranchingPreprocessor where
           pure h
       else
         pure h
-    withNewMCtxDepth <| AtomM.run .reducible <| do
+    withNewMCtxDepth <| AtomM.run .reducible do
     let nonnegs ← l.foldlM (init := ∅) fun (es : TreeSet (Nat × Nat) lexOrd.compare) h => do
       try
         let (_, _, a, b) ← (← inferType h).ineq?

Mathlib/Tactic/NormNum/Prime.lean

@@ -34,7 +34,7 @@ theorem not_prime_mul_of_ble (a b n : ℕ) (h : a * b = n) (h₁ : a.ble 1 = fal
 
 /-- Produce a proof that `n` is not prime from a factor `1 < d < n`. `en` should be the expression
   that is the natural number literal `n`. -/
-def deriveNotPrime (n d : ℕ) (en : Q(ℕ)) : Q(¬ Nat.Prime $en) := Id.run <| do
+def deriveNotPrime (n d : ℕ) (en : Q(ℕ)) : Q(¬ Nat.Prime $en) := Id.run do
   let d' : ℕ := n / d
   let prf : Q($d * $d' = $en) := (q(Eq.refl $en) : Expr)
   let r : Q(Nat.ble $d 1 = false) := (q(Eq.refl false) : Expr)

Mathlib/Tactic/Simps/Basic.lean

@@ -801,12 +801,12 @@ Optionally, this command accepts three optional arguments:
 def getRawProjections (stx : Syntax) (str : Name) (traceIfExists : Bool := false)
     (rules : Array ProjectionRule := #[]) (trc := false) :
     CoreM (List Name × Array ProjectionData) := do
-  withOptions (· |>.updateBool `trace.simps.verbose (trc || ·)) <| do
+  withOptions (·.updateBool `trace.simps.verbose (trc || ·)) do
   let env ← getEnv
   if let some data := (structureExt.getState env).find? str then
     -- We always print the projections when they already exists and are called by
     -- `initialize_simps_projections`.
-    withOptions (· |>.updateBool `trace.simps.verbose (traceIfExists || ·)) <| do
+    withOptions (·.updateBool `trace.simps.verbose (traceIfExists || ·)) do
       trace[simps.verbose]
         projectionsInfo data.2.toList "The projections for this structure have already been \
         initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.\n\
@@ -1193,7 +1193,7 @@ If `shortNm` is true, the generated names will only use the last projection name
 If `trc` is true, trace as if `trace.simps.verbose` is true. -/
 def simpsTac (ref : Syntax) (nm : Name) (cfg : Config := {})
     (todo : List (String × Syntax) := []) (trc := false) : AttrM (Array Name) :=
-  withOptions (· |>.updateBool `trace.simps.verbose (trc || ·)) <| do
+  withOptions (·.updateBool `trace.simps.verbose (trc || ·)) do
   let env ← getEnv
   let some d := env.find? nm | throwError "Declaration {nm} doesn't exist."
   let lhs : Expr := mkConst d.name <| d.levelParams.map Level.param