mathlib

mathlib copied to clipboard

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