fix: rewrite tactic should not try to synthesize instances that have been inferred by unification (#3509)

src/Lean/Meta/Tactic/Rewrite.lean

@@ -52,7 +52,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let u1 ← getLevel α
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
-          postprocessAppMVars `rewrite mvarId newMVars binderInfos
+          postprocessAppMVars `rewrite mvarId newMVars binderInfos (synthAssignedInstances := false)
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)

tests/lean/run/rw_inst_implicit_args.lean

@@ -0,0 +1,15 @@
+/-
+This test ensures `rw` will not try to synthesize instance implicit arguments when they can
+be inferred by unification. Note that in some cases the inferred instance may not even be
+definitionally equal to the inferred one, and would prevent the rewrite from being applied.
+-/
+theorem dec_and (p q : Prop) [Decidable (p ∧ q)] [Decidable p] [Decidable q] : decide (p ∧ q) = (p && q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+theorem dec_not (p : Prop) [Decidable (¬p)] [Decidable p] : decide (¬p) = !p := by
+  by_cases p <;> simp [*]
+
+example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by
+  simp only [imp_false]
+  rw [dec_and]
+  rw [dec_not]