assoc_rw can leave side-goals as metavariables

[alexjbest]

e.g.

import group_theory.basic
example {G : Type*} [add_comm_group G] (h : ∀ (g :G) (t : g ≠ 0), g + g =0) (g f : G): f + g + g = f :=
begin
assoc_rw h g,
exact add_zero _,
end

fails with tactic failed, result contains meta-variables as h g needs g \ne 0, but that is never spawned as goal.

[alexjbest]

The same this happens with nth_rewrite, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Linear.20algebra.20problem/near/281071517