Can't synthesize FTCFilter

Stream: new members

[Michael Kielstra]

Hi all,

I've got a function defined on Set.Icc a b and I'd like to use the HasDerivWithinAt version of the Fundamental Theorem of Calculus. However, whenever I try to apply integral_hasDerivWithinAt_right, which seems like the right theorem to use, I get an error that starts with Failed to synthesize FTCFilter... I don't completely understand the design of the Mathlib library here: FTCFilter seems like a tool to allow Lean to automatically pick which version of FToC to apply? Whatever it is, how do I get Lean to make one for me? Minimal (not) working example, including error text:

import Mathlib.Tactic

open intervalIntegral

example {f : ℝ → ℝ} {x a b : ℝ} (h_f: ContinuousOn f (Set.Icc a b)) (h_xinab: x ∈ Set.Icc a b) :
  HasDerivWithinAt (∫ y in a.. · , f y) (f x) (Set.Icc a b) x := by
  apply integral_hasDerivWithinAt_right (t := Set.Icc a b)
  -- Exact error given:
  -- failed to synthesize
  --  FTCFilter x (nhdsWithin x (Set.Icc a b)) (nhdsWithin x (Set.Icc a b))
  -- But the definition of FTCFilter.nhdsIcc is exactly
  --  FTCFilter x (nhdsWithin x (Set.Icc a b)) (nhdsWithin x (Set.Icc a b))
  -- And the only required proposition is that x ∈ Set.Icc a b, which is just h_xinab.
  sorry

It works if I replace Set.Icc a b with Set.Iic b, but I don't think that works for me because f is only continuous etc on Set.Icc a b.

Thanks!

[Thomas Browning]

I think the issue is that docs#intervalIntegral.FTCFilter.nhdsIcc requires an instance Fact (x ∈ Set.Icc a b). So if you turn h_xinab into a fact instance, then everything should work:

import Mathlib.Tactic

open intervalIntegral

example {f : ℝ → ℝ} {x a b : ℝ} (h_f: ContinuousOn f (Set.Icc a b)) (h_xinab: x ∈ Set.Icc a b) :
  HasDerivWithinAt (∫ y in a.. · , f y) (f x) (Set.Icc a b) x := by
  have := Fact.mk h_xinab
  apply integral_hasDerivWithinAt_right (t := Set.Icc a b)
  sorry

[Thomas Browning]

(the only difference between P and Fact P is that Fact P is an instance and can be found automatically by Lean).