-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurable_derivWithin_Ici [MeasurableSpace F] [BorelSpace F] :
    Measurable fun x => derivWithin f (Ici x) x

Proof state:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x => derivWithin f (Ici x) x

Tactic:
refine measurable_of_isClosed fun s hs => ?_

Result:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
⊢ MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)

Proof state:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
this :
  (fun x => derivWithin f (Ici x) x) ⁻¹' s =
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet
    ({x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s})

Tactic:
exact
  (measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
    ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

Result:
no goals

Proof state:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
⊢ MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)

Tactic:
have :
  (fun x => derivWithin f (Ici x) x) ⁻¹' s =
    { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s } ∪
      { x | ¬DifferentiableWithinAt ℝ f (Ici x) x } ∩ { _x | (0 : F) ∈ s } :=
  Set.ext fun x => mem_preimage.trans derivWithin_mem_iff

Result:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
this :
  (fun x => derivWithin f (Ici x) x) ⁻¹' s =
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)

Proof state:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
this :
  (fun x => derivWithin f (Ici x) x) ⁻¹' s =
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)

Tactic:
rw [this]

Result:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed s
this :
  (fun x => derivWithin f (Ici x) x) ⁻¹' s =
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet
    ({x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s})