squeeze_simp reports spurious `eq_self_iff_true`

Stream: general

[Scott Morrison]

@Simon Hudon, are you aware of the bug in squeeze_simp whereby it very often spuriously reports eq_self_iff_true? If not, I'll provide some MWEs.

[Mario Carneiro]

simp has some basic set of lemmas that it uses even if you don't say anything

[Mario Carneiro]

I'm not exactly sure what the list is

[Johan Commelin]

Aha, that's good to know. But those shouldn't be reported in the output of squeeze_simp, I guess.

[Simon Hudon]

It should be easy to fix.

[Simon Hudon]

I just created #1047. It also removes overlap between suggestions and the arguments you're already providing.