diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 19d35363cb..f9af107abd 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -40,10 +40,9 @@ def Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result :=
 
 /-- Flip the proof in a `Simp.Result`. -/
 def Result.mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
-  ({ expr := e, proof? := · }) <$>
   match r.proof? with
-  | none => pure none
-  | some p => some <$> Meta.mkEqSymm p
+  | none   => return { r with expr := e }
+  | some p => return { r with expr := e, proof? := some (← Meta.mkEqSymm p) }
 
 abbrev Cache := ExprMap Result