E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x : E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ n c x
hr : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ n g x
⊢ ∀ (x : X), ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x : E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ n c
hr : ContDiff ℝ n fun x => (f x).rIn
hR : ContDiff ℝ n fun x => (f x).rOut
hg : ContDiff ℝ n g
⊢ ContDiff ℝ n fun x => ↑(f x) (g x)
rw [contDiff_iff_contDiffAt] at *
no goals
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x : E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ n c x
hr : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ n g x
⊢ ∀ (x : X), ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)