From 8a8a8b5e48e7b6b4007ad40e0e9b9b94e6ea67d6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jun 2022 18:27:43 -0700
Subject: [PATCH] chore: style

---
 src/Lean/Elab/Tactic/Conv/Congr.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index a876677400..8a91b0ae4f 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -11,7 +11,7 @@ open Meta
 
 /-- Returns a list of new congruence subgoals, which contains `none` for each argument with
 forward dependencies. -/
-private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List $ Option MVarId) :=
+private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MVarId)) :=
   -- TODO: add support for `[congr]` lemmas
   lhs.withApp fun f args => do
     let infos := (← getFunInfoNArgs f args.size).paramInfo
@@ -55,21 +55,21 @@ def isImplies (e : Expr) : MetaM Bool :=
   else
     return false
 
-def congr (mvarId : MVarId) : MetaM (List $ Option MVarId) :=
+def congr (mvarId : MVarId) : MetaM (List (Option MVarId)) :=
   withMVarContext mvarId do
     let (lhs, rhs) ← getLhsRhsCore mvarId
     let lhs := (← instantiateMVars lhs).consumeMData
     if (← isImplies lhs) then
-      pure $ (← congrImplies mvarId).map Option.some
+      return (← congrImplies mvarId).map Option.some
     else if lhs.isApp then
       congrApp mvarId lhs rhs
     else
       throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
 
 @[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
-   replaceMainGoal $ List.filterMap id (← congr (← getMainGoal))
+   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
 
-private def selectIdx (tacticName : String) (mvarIds : List $ Option MVarId) (i : Int) :
+private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
   if i >= 0 then
     let i := i.toNat