-- Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
theorem MDifferentiableWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
    (hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x)
    (hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x) :
    MDifferentiableWithinAt I 𝓘(𝕜, F₂) (fun x => g x (f x)) s x :=
  DifferentiableWithinAt.comp_mdifferentiableWithinAt (t := univ)
    (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
    (by apply (Differentiable.differentiableAt _).differentiableWithinAt
        exact differentiable_fst.clm_apply differentiable_snd) (hg.prod_mk_space hf)
    (by simp_rw [mapsTo_univ])

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x
hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x
⊢ MapsTo (fun x => (g x, f x)) s univ

Tactic:
simp_rw [mapsTo_univ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x
hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x
⊢ Differentiable 𝕜 fun x => x.1 x.2

Tactic:
exact differentiable_fst.clm_apply differentiable_snd

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x
hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x
⊢ DifferentiableWithinAt 𝕜 (fun x => x.1 x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x
hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x
⊢ Differentiable 𝕜 fun x => x.1 x.2