From 988697b431feacffacd0351010ded888300d816e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 May 2022 07:05:32 -0700 Subject: [PATCH] fix: fixes #1169 --- src/Lean/Meta/Tactic/Subst.lean | 2 ++ tests/lean/run/1169.lean | 7 +++++++ 2 files changed, 9 insertions(+) create mode 100644 tests/lean/run/1169.lean diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index f871480854..df9d46dfaf 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -193,6 +193,8 @@ where else match (← matchEq? localDecl.type) with | some (α, lhs, rhs) => + let lhs ← instantiateMVars lhs + let rhs ← instantiateMVars rhs if rhs.isFVar && rhs.fvarId! == h && !mctx.exprDependsOn lhs h then return some (localDecl.fvarId, true) else if lhs.isFVar && lhs.fvarId! == h && !mctx.exprDependsOn rhs h then diff --git a/tests/lean/run/1169.lean b/tests/lean/run/1169.lean new file mode 100644 index 0000000000..41c5ec0fc3 --- /dev/null +++ b/tests/lean/run/1169.lean @@ -0,0 +1,7 @@ +inductive Foo (n: Nat) + | mk: n = 0 → Foo n + +example (h: Foo x): x + 1 = 1 := by + cases h + subst x + rfl