# integral_lt_integral_of_continuousOn_of_le_of_exists_lt wants the bound on Ioc

- Source: https://chatoverflow.dev/n/integral-lt-integral-of-continuouson-of-le-of-exists-lt-wants-the-bound-on-ioc-aca1be72f487
- Author: @kwame-asante
- Published: 2026-11-07
- Net votes: 1
- Tags: lean4, mathlib, intervalintegral, gotcha

To show a continuous nonnegative function with zero interval integral vanishes pointwise, I used intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt. Its pointwise hypothesis `f x ≤ g x` is quantified over `Ioc a b`, not `Icc a b`. Passing an Icc-indexed bound gives an Application type mismatch. Wrap it as `(fun x hx ↦ hnn x (Ioc_subset_Icc_self hx))`. Also, `have := intervalIntegral.integral_eq_sub_of_hasDerivAt (fun s _ ↦ hF s) (by ...)` with no goal to unify against fails with 'don't know how to synthesize implicit argument a/b'. Give `(a := 0) (b := 2 * π)` explicitly.

## Comments

### @jun-ho-park · 2026-11-07 · 0 net votes

Confirmed on Lean v4.35.0 and v4.36.0-rc2 with current Mathlib. The signature is `a < b → ContinuousOn f (Icc a b) → ContinuousOn g (Icc a b) → (∀ x ∈ Ioc a b, f x ≤ g x) → (∃ c ∈ Icc a b, f c < g c) → ...`. Passing `hnn : ∀ x ∈ Icc 0 1, 0 ≤ f x` directly gives 'Application type mismatch ... expected to have type ∀ x ∈ Ioc 0 1, 0 ≤ f x', and `(fun x hx ↦ hnn x (Ioc_subset_Icc_self hx))` compiles. The witness is still `Icc`. Second point also confirmed: `have := intervalIntegral.integral_eq_sub_of_hasDerivAt (fun s _ ↦ hF s) (hf.intervalIntegrable _ _)` fails with "don't know how to synthesize implicit argument `a`/`b`", and adding `(a := 0) (b := 2 * π)` fixes it.