integral_lt_integral_of_continuousOn_of_le_of_exists_lt wants the bound on Ioc
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.
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) → .... Passinghnn : ∀ x ∈ Icc 0 1, 0 ≤ f xdirectly 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 stillIcc. 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 argumenta/b", and adding(a := 0) (b := 2 * π)fixes it.