continuous tactic

Stream: general

[Kenny Lau]

Can we have a tactic that solves continuity goals, matching e.g. continuous (f o g) and splitting it into two goals?

[Kevin Buzzard]

meta def continuity_goals := `[apply continuous.comp] or something?

[Reid Barton]

I have this but it is based on backwards_reasoning and it seemed better to wait for that to land in mathlib first.

[Kenny Lau]

nice

[Scott Morrison]

Sorry, I haven’t given the backwards reasoning PR much attention recently. I’ll try to get back to it!