function cont diffable from set to internal

Stream: new members

[Abu Al Hassan]

Hello, I have a function such that it's continuous on a segment from some point x_star to some other point x_star + α • d. Where x_star and d are vectors and α is real. Then I should be able to write this such as the following where the function only takes in a input c in reals in a interval [0, α] and scales d by c and transforms it by x_star.

import tactic -- imports all the Lean tactics
import data.real.basic -- imports the real numbers
import analysis.calculus.cont_diff
open set

-- Declare a type E with some properties
variables (E : Type*) [normed_add_comm_group E] [normed_space ℝ E]

theorem MWE (f : E → ℝ) (u : set E) (h_open : is_open u) (α: ℝ) (x_star d: E)
(h_xstar: x_star ∈ u) (h_d_not_zero: d ≠ 0) (h_d_in_u: d ∈ u)
(h_twice_continuous_diffable: cont_diff_on ℝ 2 (λ (x : E), f x) (segment ℝ x_star (x_star + α • d)))  :
cont_diff_on ℝ 2 (λ (c : ℝ), f (x_star + c • d)) (Icc 0 α) :=
begin
sorry,
end

I would have thought there is some 'rw ___' command I can use to show this is essentially equivalent to 'h_twice_continuous_diffable' but maybe i am wrong and i have to do this in a multistep proof.

[Sebastien Gouezel]

Can you use docs#cont_diff_on.comp?

[Abu Al Hassan]

Thank you, Sebastien! This is exactly what I was looking for. Got it to work.