Failure to prove simple result about continuous functions

[PatrickMassot]

Desired proof term

Please construct the proof term that Canonical should generate, such that the goal is closed. The term should not contain let definitions, and should be fewer than 100 "words". For example:

import Mathlib.Data.Real.Basic

def continuous_function_at (f : ℝ → ℝ) (x₀ : ℝ) :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (hf ε ε_pos).elim
   fun δ ⟨δ_pos, hδ⟩ ↦ (hu δ δ_pos).elim
     fun N hN ↦ ⟨N, fun n n_ge ↦ hδ (u n) <| hN n n_ge⟩

Canonical invocation

canonical +debug [continuous_function_at, sequence_tendsto, Exists.elim]

With a high enough heartbeat setting, this generates a 225Mb debug.json that GitHub refuses to upload.

Observations

Let us know if you believe a particular aspect of the problem is responsible for the failure. Common issues include:

1. Reasoning with the "arrow" type constructor (add +pi).
2. Canonical does not currently support the Eta law for structures.
3. Speculative use of a function with reduction behavior (add +synth once stable).
4. "Explosive" recursive unfolding of complex definitions that should be opaque.

Adding +pi doesn’t seem to help. The debug log certainly suggests recursive unfolding of complex definition.