From 881bf2a088ad36db66aaee4e497f6860a4c3164b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Oct 2021 14:14:49 -0700
Subject: [PATCH] fix: set `zeta` to true at `pattern` conv tactic

---
 src/Lean/Elab/Tactic/Conv/Pattern.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean
index c643285c68..e7daa03a03 100644
--- a/src/Lean/Elab/Tactic/Conv/Pattern.lean
+++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean
@@ -13,7 +13,10 @@ private def getContext : MetaM Simp.Context := do
   return {
     simpLemmas    := {}
     congrLemmas   := (← getCongrLemmas)
-    config.zeta   := false
+    /-
+     The `pattern` conv tactic is based on `conv`, and rewriting `let` terms may produce type incorrect results.
+    -/
+    config.zeta   := true
     config.beta   := false
     config.eta    := false
     config.iota   := false