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