diff --git a/Mathlib/Lean/Meta.lean b/Mathlib/Lean/Meta.lean
index afd5eae054996..b08a6e9862aa5 100644
--- a/Mathlib/Lean/Meta.lean
+++ b/Mathlib/Lean/Meta.lean
@@ -41,7 +41,7 @@ def applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (Lis
 def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
   es.foldlM (λ mv e => do
       let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mv do
-        Elab.Tactic.evalTactic (←`(tactic| refine ⟨?_,?_⟩))
+        Elab.Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
       let [sg1, sg2] := subgoals | throwError "expected two subgoals"
       sg1.assign e
       pure sg2)
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
index 32c2093e91f6d..3fb71eeb4a499 100644
--- a/Mathlib/Tactic/Lift.lean
+++ b/Mathlib/Tactic/Lift.lean
@@ -149,7 +149,7 @@ def Lift.main (e t : TSyntax `term) (hUsing : Option (TSyntax `term))
     (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal)
   -- if we use a new variable, then substitute it everywhere
   if isNewVar then
-    for decl in ←getLCtx do
+    for decl in ← getLCtx do
       if decl.userName != newEqName then
         let declIdent := mkIdent decl.userName
         -- The line below fails if $declIdent is there only once.
diff --git a/Mathlib/Tactic/Linarith/Datatypes.lean b/Mathlib/Tactic/Linarith/Datatypes.lean
index d4ecf3d941000..ef58dd239bd52 100644
--- a/Mathlib/Tactic/Linarith/Datatypes.lean
+++ b/Mathlib/Tactic/Linarith/Datatypes.lean
@@ -318,7 +318,7 @@ open Meta
 structure LinarithConfig : Type where
   /-- Discharger to prove that a candidate linear combination of hypothesis is zero. -/
   -- TODO There should be a def for this, rather than calling `evalTactic`?
-  discharger : TacticM Unit := do evalTactic (←`(tactic| ring1))
+  discharger : TacticM Unit := do evalTactic (← `(tactic| ring1))
   -- We can't actually store a `Type` here,
   -- as we want `LinarithConfig : Type` rather than ` : Type 1`,
   -- so that we can define `elabLinarithConfig : Lean.Syntax → Lean.Elab.TermElabM LinarithConfig`.
@@ -346,7 +346,7 @@ since this is typically needed when using stronger unification.
 def LinarithConfig.updateReducibility (cfg : LinarithConfig) (reduce_default : Bool) :
     LinarithConfig :=
   if reduce_default then
-    { cfg with transparency := .default, discharger := do evalTactic (←`(tactic| ring1!)) }
+    { cfg with transparency := .default, discharger := do evalTactic (← `(tactic| ring1!)) }
   else cfg
 
 /-!
diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean
index 4606e4367f25f..c28374a2d10db 100644
--- a/Mathlib/Tactic/MkIffOfInductiveProp.lean
+++ b/Mathlib/Tactic/MkIffOfInductiveProp.lean
@@ -144,8 +144,8 @@ do let type := (← getConstInfo c).instantiateTypeLevelParams univs
      let eqs ← eqs.mapM (λ⟨idx, inst⟩ => do
           let ty ← idx.fvarId!.getType
           let instTy ← inferType inst
-          let u := (←inferType ty).sortLevel!
-          if ←isDefEq ty instTy
+          let u := (← inferType ty).sortLevel!
+          if ← isDefEq ty instTy
           then pure (mkApp3 (mkConst `Eq [u]) ty idx inst)
           else pure (mkApp4 (mkConst `HEq [u]) ty idx instTy inst))
      let (n, r) ← match bs.filterMap id, eqs with
@@ -153,7 +153,7 @@ do let type := (← getConstInfo c).instantiateTypeLevelParams univs
            pure (some 0, (mkConst `True))
      | bs', [] => do
           let t : Expr ← bs'.getLast!.fvarId!.getType
-          let l := (←inferType t).sortLevel!
+          let l := (← inferType t).sortLevel!
           if l == Level.zero then do
             let r ← mkExistsList (List.init bs') t
             pure (none, subst r)
@@ -172,15 +172,15 @@ def splitThenConstructor (mvar : MVarId) (n : Nat) : MetaM Unit :=
 match n with
 | 0   => do
   let (subgoals',_) ← Term.TermElabM.run $ Tactic.run mvar do
-    Tactic.evalTactic (←`(tactic| constructor))
+    Tactic.evalTactic (← `(tactic| constructor))
   let [] := subgoals' | throwError "expected no subgoals"
   pure ()
 | n + 1 => do
   let (subgoals,_) ← Term.TermElabM.run $ Tactic.run mvar do
-    Tactic.evalTactic (←`(tactic| refine ⟨?_,?_⟩))
+    Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
   let [sg1, sg2] := subgoals | throwError "expected two subgoals"
   let (subgoals',_) ← Term.TermElabM.run $ Tactic.run sg1 do
-    Tactic.evalTactic (←`(tactic| constructor))
+    Tactic.evalTactic (← `(tactic| constructor))
   let [] := subgoals' | throwError "expected no subgoals"
   splitThenConstructor sg2 n
 
@@ -277,7 +277,7 @@ def toInductive (mvar : MVarId) (cs : List Name)
                                    ) mv3
            pure (mv4, fvars)
         mvar'.withContext do
-          let fvarIds := (←getLCtx).getFVarIds.toList
+          let fvarIds := (← getLCtx).getFVarIds.toList
           let gs := fvarIds.take gs.length
           let hs := (fvarIds.reverse.take n).reverse
           let m := gs.map some ++ listBoolMerge bs hs
@@ -311,7 +311,7 @@ def mkIffOfInductivePropImpl (ind : Name) (rel : Name) (relStx : Syntax) : MetaM
     let fvars' := fvars.toList
     let shape_rhss ← constrs.mapM (constrToProp univs (fvars'.take params) (fvars'.drop params))
     let (shape, rhss) := shape_rhss.unzip
-    pure (←mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)),
+    pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)),
           shape)
 
   let mvar ← mkFreshExprMVar (some thmTy)
diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean
index 2e453cd7d3b07..0d6a1fadbed47 100644
--- a/Mathlib/Tactic/Nontriviality/Core.lean
+++ b/Mathlib/Tactic/Nontriviality/Core.lean
@@ -27,7 +27,7 @@ including `Subsingleton.le` and `eq_iff_true_of_subsingleton`.
 -/
 def nontrivialityByElim (α : Q(Type u)) (g : MVarId) (simpArgs : Array Syntax) : MetaM MVarId := do
   let p : Q(Prop) ← g.getType
-  guard (←instantiateMVars (← inferType p)).isProp
+  guard (← instantiateMVars (← inferType p)).isProp
   g.withContext do
     let g₁ ← mkFreshExprMVarQ q(Subsingleton $α → $p)
     let (_, g₁') ← g₁.mvarId!.intro1
diff --git a/Mathlib/Tactic/PushNeg.lean b/Mathlib/Tactic/PushNeg.lean
index b5875a12442a3..fb21cadfd33da 100644
--- a/Mathlib/Tactic/PushNeg.lean
+++ b/Mathlib/Tactic/PushNeg.lean
@@ -77,12 +77,12 @@ def transformNegationStep (e : Expr) : SimpM (Option Simp.Step) := do
       return mkSimpStep e (← mkAppM ``not_not_eq #[e])
   | (``And, #[p, q]) =>
       match ← getBoolOption `push_neg.use_distrib with
-      | false => return mkSimpStep (.forallE `_ p (mkNot q) default) (←mkAppM ``not_and_eq #[p, q])
-      | true  => return mkSimpStep (mkOr (mkNot p) (mkNot q)) (←mkAppM ``not_and_or_eq #[p, q])
+      | false => return mkSimpStep (.forallE `_ p (mkNot q) default) (← mkAppM ``not_and_eq #[p, q])
+      | true  => return mkSimpStep (mkOr (mkNot p) (mkNot q)) (← mkAppM ``not_and_or_eq #[p, q])
   | (``Or, #[p, q]) =>
-      return mkSimpStep (mkAnd (mkNot p) (mkNot q)) (←mkAppM ``not_or_eq #[p, q])
+      return mkSimpStep (mkAnd (mkNot p) (mkNot q)) (← mkAppM ``not_or_eq #[p, q])
   | (``Iff, #[p, q]) =>
-      return mkSimpStep (mkOr (mkAnd p (mkNot q)) (mkAnd (mkNot p) q)) (←mkAppM ``not_iff #[p, q])
+      return mkSimpStep (mkOr (mkAnd p (mkNot q)) (mkAnd (mkNot p) q)) (← mkAppM ``not_iff #[p, q])
   | (``Eq, #[ty, e₁, e₂]) =>
       if ty.isAppOfArity ``Set 1 then
         -- test if equality is of the form `s = ∅`, and negate it to `s.Nonempty`
diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
index 3042002b3e5dd..fb1869a4e04fe 100644
--- a/Mathlib/Tactic/Rewrites.lean
+++ b/Mathlib/Tactic/Rewrites.lean
@@ -246,7 +246,7 @@ def rewritesCore (hyps : Array (Expr × Bool × Nat))
     let some expr ← (match lem with
     | .inl hyp => pure (some hyp)
     | .inr lem => try? <| mkConstWithFreshMVarLevels lem) | return none
-    trace[Tactic.rewrites] m!"considering {if symm then "←" else ""}{expr}"
+    trace[Tactic.rewrites] m!"considering {if symm then "← " else ""}{expr}"
     let some result ← try? do goal.rewrite target expr symm
       | return none
     if result.mvarIds.isEmpty then
diff --git a/Mathlib/Tactic/SimpRw.lean b/Mathlib/Tactic/SimpRw.lean
index e64106927c561..5c3728ea44ce8 100644
--- a/Mathlib/Tactic/SimpRw.lean
+++ b/Mathlib/Tactic/SimpRw.lean
@@ -67,6 +67,6 @@ elab s:"simp_rw " cfg:(config)? rws:rwRuleSeq g:(location)? : tactic => do
     evalTactic (← match term with
     | `(term| $e:term) =>
       if symm then
-        `(tactic| simp%$e $[$cfg]? only [←$e:term] $g ?)
+        `(tactic| simp%$e $[$cfg]? only [← $e:term] $g ?)
       else
         `(tactic| simp%$e $[$cfg]? only [$e:term] $g ?))
diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean
index 7160870a60054..a721fbcc8773a 100644
--- a/Mathlib/Tactic/SplitIfs.lean
+++ b/Mathlib/Tactic/SplitIfs.lean
@@ -81,7 +81,7 @@ private def splitIf1 (cond : Expr) (hName : Name) (loc : Location) : TacticM Uni
 list is empty.
 -/
 private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : MetaM Name := do
-  match ←hNames.get with
+  match ← hNames.get with
   | [] => mkFreshUserName `h
   | n::ns => do hNames.set ns
                 if let `(binderIdent| $x:ident) := n
@@ -104,7 +104,7 @@ private partial def splitIfsCore
     (hNames : IO.Ref (List (TSyntax `Lean.binderIdent))) :
     List Expr → TacticM Unit := fun done ↦ withMainContext do
   let some (_,cond) ← findIfCondAt loc
-      | Meta.throwTacticEx `split_ifs (←getMainGoal) "no if-then-else conditions to split"
+      | Meta.throwTacticEx `split_ifs (← getMainGoal) "no if-then-else conditions to split"
 
   -- If `cond` is `¬p` then use `p` instead.
   let cond := if cond.isAppOf `Not then cond.getAppArgs[0]! else cond
diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
index f9ff93dc14ce0..88bde8ecc1ef6 100644
--- a/Mathlib/Tactic/Tauto.lean
+++ b/Mathlib/Tactic/Tauto.lean
@@ -169,7 +169,7 @@ def tautoCore : TacticM Unit := do
       distribNot <;>
       liftMetaTactic (casesMatching casesMatcher (recursive := true) (throwOnNoMatch := false)) <;>
       (do _ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;>
-      (do _ ← tryTactic (evalTactic (←`(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
+      (do _ ← tryTactic (evalTactic (← `(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
       liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;>
       liftMetaTactic (constructorMatching · coreConstructorMatcher
         (recursive := true) (throwOnNoMatch := false)) <;>
diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean
index c8df05dbd74a0..aa268c2bdcdf2 100644
--- a/Mathlib/Tactic/Widget/Conv.lean
+++ b/Mathlib/Tactic/Widget/Conv.lean
@@ -30,7 +30,7 @@ private def solveLevel (expr : Expr) (path : List Nat) : MetaM SolveReturn := ma
     -- we go through the application until we reach the end, counting how many explicit arguments
     -- it has and noting whether they are explicit or implicit
     while descExp.isApp do
-      if (←Lean.Meta.inferType descExp.appFn!).bindingInfo!.isExplicit then
+      if (← Lean.Meta.inferType descExp.appFn!).bindingInfo!.isExplicit then
         explicitList := true::explicitList
         count := count + 1
       else