Tactics for topology
Currently we have one domain-specific tactic for topology:
Automatically solve goals of the form
Tactic to apply
continuous.comp when appropriate.
continuous.comp is not always a good idea, so we have some
extra logic here to try to avoid bad cases.
If the function we're trying to prove continuous is actually constant, and that constant is a function application
f z, then continuous.comp would produce new goals
continuous (λ _, z), which is silly. We avoid this by failing if we could apply continuous_const.
Solve goals of the form
continuity? reports back the proof term it found.