continuity and ContinuousOn

Stream: mathlib4

[Michael Stoll]

import Mathlib

example : ContinuousOn (fun t : ℝ ↦ t) (Set.Icc 0 1) := by
  continuity -- "tactic 'aesop' failed, failed to prove the goal after exhaustive search."
  sorry

Is continuitynot supposed to work for goals of the shape ContinuousOn ...?
How can I massage the goal so that continuityworks?

[Ruben Van de Velde]

If your function actually is everywhere continuous:

import Mathlib

example : ContinuousOn (fun t : ℝ ↦ t) (Set.Icc 0 1) := by
  apply Continuous.continuousOn
  continuity

[Michael Stoll]

And what if it isn't?

[Michael Stoll]

My use case is more like

z: ℂ
⊢ ContinuousOn (fun t : ℝ ↦ t * (1 + t * z)⁻¹) (Set.Icc 0 1)

(and I can show that 1 + t * z does not vanish on the relevant interval).

[Junyan Xu]

You can apply docs#ContinuousAt.continuousOn and then docs#ContinuousAt.mul and docs#ContinuousAt.inv₀. An automated tactic could possibly solve this by just "unfolding" the definition of ContinuousOn (intro t ht) and apply the ContinuousWithinAt lemmas.

[Michael Stoll]

I know how I can do it by hand. Ideally, continuity would essentially do what you suggest and leave the side goals that need to be closed for things like divisions to be filled later. But I assume that does not work with aesop, as aesop is a finishing tactic?

[Heather Macbeth]

I believe it's possible to turn off backtracking in Aesop. In this case I believe it can be used as a non-finishing tactic.

[Heather Macbeth]

You can also look into apply_rules for an overlapping set of functionality.

[Heather Macbeth]

In my opinion, the best way to make a non-finishing tactic for this kind of task is to make it be fairly opinionated but to offer a pattern syntax which makes it easy for the user to specify a non-default desired level of operation on the tree of the expression. This is what gcongr does.

[Heather Macbeth]

So you could say continuity log (?_ + 1) to get it to use the log, add and const lemmas and present the rest as a goal.

[Michael Stoll]

It would be nice if somebody could do that :-)

[Bhavik Mehta]

I'm in favour of a pattern syntax for this too

[Michael Stoll]

Could continuity be made to work here?

example : Continuous (fun z : ℂ ↦ (2 : ℂ) ^ z) := by continuity

(The problem likely is that docs#Continuous.const_cpow needs that 2 is not zero...)

[Kevin Buzzard]

Unlikely to help but you could put a proof of (2 : \C) \ne 0 into the context and try again...