fix(library/init/meta/interactive): use replace_target at simp_goal

replace_target uses id_locked.
The id_locked solution is more robust because simp may build a proof
using refl lemmas, but type_context may not be able to establish that
the previous and new target are definitionally equal.

@Armael This commit fixes the issue in the KreMLin proof you showed me.
Now, the following tactic succeeds (as expected)
```
        simp [lowstar_semantics.apply_ectx],
```
and the resulting goal is
```
...
|- exp.subbuf (exp.loc (b, n, list.nil field)) a_1 = exp.subbuf ↑?m_1 ?m_2
```

library/init/data/nat/lemmas.lean

@@ -38,7 +38,7 @@ protected lemma add_comm : ∀ n m : ℕ, n + m = m + n
 
 protected lemma add_assoc : ∀ n m k : ℕ, (n + m) + k = n + (m + k)
 | n m 0        := rfl
-| n m (succ k) := by simp [add_succ, add_assoc n m k]
+| n m (succ k) := by rw [add_succ, add_succ, add_assoc]
 
 protected lemma add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k) :=
 left_comm nat.add nat.add_comm nat.add_assoc

library/init/meta/interactive.lean

@@ -677,10 +677,8 @@ open interactive interactive.types expr
 
 private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit
 | s := do
-   (new_target, Heq) ← target >>= simplify_core cfg s `eq,
-   tactic.assert `Htarget new_target, swap,
-   Ht ← get_local `Htarget,
-   mk_eq_mpr Heq Ht >>= tactic.exact
+   (new_target, pr) ← target >>= simplify_core cfg s `eq,
+   replace_target new_target pr
 
 private meta def simp_hyp (cfg : simp_config) (s : simp_lemmas) (h_name : name) : tactic unit :=
 do h     ← get_local h_name,