apply? and equalities

Stream: mathlib4

[Johan Commelin]

Andrew Yang said:

IIRC apply? does not work for goals about equalities

I didn't check this. But if it is true, then it would be great if apply? would throw a warning: "Your goal is an equality. I don't deal with those."

[Kim Morrison]

If true, that would be a bug. It doesn't work with goals of the form x = y, where the type is a variable. But any structure on either the lhs or rhs, or structure in the type, should allow it to run.

[Kim Morrison]

I guess there could be a useful message in that case, however. PR welcome. :-)