From 414f0eb19b8aca0d357c36685334694a859d59bf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 5 Mar 2024 06:37:09 -0800
Subject: [PATCH] fix: bug at `Result.mkEqSymm` (#3606)

`cache` and `dischargeDepth` fields were being reset.
---
 src/Lean/Meta/Tactic/Simp/Types.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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