squeeze_simp also simplify targets

[alexjbest]

Currently squeeze_simp [blah] at * reduces the list of lemmas applied to only those that are actually applied, but still applies to all hypotheses and the goal. It would be nice to have squeeze_simp also prune the list of targets after at to only those that the lemmas where things are actually applied. e.g. squeeze_simp would output simp only [blah] at \|- h g,.

example (h : 1 + 1 = 2) : 1 - 1 = 0 :=
begin
  squeeze_simp at *,  --desired output   simp only [eq_self_iff_true] at \|-, or   simp only [eq_self_iff_true],
end

[cipher1024]

Why is this useful?

[alexjbest]

Its clearer to the (human) reader whats going on in the proof was my main thought, especially when there are many hypotheses.

If you have many hypotheses this could be more efficient for the simplifier, this is probably negligible though, what do you think?

[cipher1024]

I feel like the performance improvement would be minimal and it might just make your proofs more brittle. You change your hypothesis names and it breaks. If you don't know which assumptions to use simp on, it might preferable to let the script adjust itself to changes.