feat(tactic/set): fix a bug (#14488)
We make the behaviour of `tactic.interactive.set` closer to that of `tactic.interactive.let`, this should fix the following issue reported in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/set.20bug.3F/near/284471523:
```lean
import ring_theory.adjoin.basic
example {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S] (x : S): false :=
begin
let y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- works
set y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- error
sorry
end
```
This is related to [lean#555
](https://github.com/leanprover-community/lean/pull/555)
I also fix two completely unrelated docstrings (where the list syntax created two lists instead of one) as I wouldn't want to separately add them to CI...
