diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index a0879ff78a..c342598938 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/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
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index dba6d6cc39..105cb05ba1 100644
--- a/library/init/meta/interactive.lean
+++ b/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,