fix: fixes #1169

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

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