refine and type class inference

Stream: general

[Johan Commelin]

Can we have a version of refine that ignores typeclasses. So I write refine my_lemma _ _ _ _ X _ _ Y, and Lean tries unification. But if it can't find a topology on X (or whatever) it doesn't complain, but just returns that as a goal.

[Johan Commelin]

Currently I just get stupid max type class errors, and I would like to easily march ahead and break this into subgoals.