fix: fixes #1856

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -151,6 +151,10 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
 
 private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   let cfg := (← read).config
+  if e.getAppFn.isMVar then
+    let e' ← instantiateMVars e
+    if e' != e then
+      return (← reduce e')
   if cfg.beta then
     let e' := e.headBeta
     if e' != e then

tests/lean/1856.lean

@@ -0,0 +1,26 @@
+structure Equiv (α : Sort _) (β : Sort _) where
+  toFun : α → β
+  invFun : β → α
+  left_inv : ∀ x, invFun (toFun x) = x
+
+infixl:25 " ≃ " => Equiv
+
+/-- A product of types can be split as the binary product of one of the types and the product
+  of all the remaining types. -/
+def piSplitAt {α : Type _} [DecidableEq α] (i : α) (β : α → Type _) :
+    (∀ j, β j) ≃ β i × ∀ j : { j // j ≠ i }, β j where
+  toFun f := ⟨f i, fun j => f j⟩
+  invFun f j := if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩
+  left_inv f := by
+    apply funext
+    intro x
+    /- Goal is now:
+    ```
+    (fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h })
+      ((fun f => (f i, fun j => f j.val)) f) x =
+      f x
+    ```
+    -/
+    dsimp
+    trace_state
+    sorry

tests/lean/1856.lean.expected.out

@@ -0,0 +1,9 @@
+1856.lean:10:4-10:13: warning: declaration uses 'sorry'
+case h
+α : Type ?u
+inst✝ : DecidableEq α
+i : α
+β : α → Type ?u
+f : (j : α) → β j
+x : α
+⊢ (if h : x = i then (_ : i = x) ▸ f i else f x) = f x