proper way to discharge DifferentiableOn deriv of comp

Stream: Is there code for X?

[ohhaimark]

I have the goal: DifferentiableOn ℝ (deriv (cos ∘ sqrt)) (Set.Ioo 0 ((π / 2) ^ 2))
I can't (rewrite/apply DifferentiableOn.congr) with deriv_comp because sqrt is not Differentiable, but I can't see an equivalent that applies chain rule on just a subset.
I can probably just brute force unfolding until I get something I can prove, but I want to know what the intended way would be.
(Also, should this be here or in the mathlib channel? The latter seems to be more for development within mathlib, but this isn't quite a "Code for X" query)

[Etienne Marion]

deriv_comp only requires DifferentiableAt, so why can’t you use DifferentiableOn.congr?

[Ruben Van de Velde]

It may help to share your question as a #mwe

[ohhaimark]

@Etienne Marion I must have read it wrong when I looked at the definition. Just a brainfart then. Apologies.

[ohhaimark]

I now have a similar problem with a 2nd derivative. I can't rewrite the inner derivative because it doesn't have bounds applied to it. MWE

[Etienne Marion]

You should post the code here, instructions are in #mwe and #backticks.

[ohhaimark]

import Mathlib
open Real

lemma goal
  (cos_sqrt_deriv : ∀ x ∈ Set.Ioo 0 ((π / 2) ^ 2), deriv (cos ∘ sqrt) x = -sin √x / (2 * √x))
  (x : ℝ)
  (x_pos : 0 < x)
  (x_lt : x < (π / 2) ^ 2) :
  0 ≤ deriv (fun y => deriv (cos ∘ sqrt) y) x := by
    sorry

Forgive my reading comprehension.

[Etienne Marion]

I think you could use Set.EqOn.deriv.