-- Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
differentiably on `m`, one can apply `ϕ m` to `g m`, and the resulting map is differentiable.

Note that the differentiability of `ϕ` can not be always be stated as differentiability of a map
into a manifold, as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only make sense when `b₁`
and `b₂` are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of `ϕ` read in coordinates.

Version for `MDifferentiableAt`. We also give a version for `MDifferentiableWithinAt`,
but no version for `MDifferentiableOn` or `MDifferentiable` as our assumption, written
in coordinates, only makes sense around a point.
-/
lemma MDifferentiableAt.clm_apply_of_inCoordinates
    (hϕ : MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂)
      (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
    (hv : MDifferentiableAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m ↦ (v m : TotalSpace F₁ E₁)) m₀)
    (hb₂ : MDifferentiableAt IM IB₂ b₂ m₀) :
    MDifferentiableAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) m₀

Proof state:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B₁) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B₂) → AddCommGroup (E₂ x)
inst✝²³ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
inst✝⁶ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ : MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m => inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : MDifferentiableAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m => { proj := b₁ m, snd := v m }) m₀
hb₂ : MDifferentiableAt IM IB₂ b₂ m₀
⊢ MDifferentiableAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m => { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hϕ hv hb₂ ⊢

Result:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B₁) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B₂) → AddCommGroup (E₂ x)
inst✝²³ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
inst✝⁶ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ :
  MDifferentiableWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m => inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    univ m₀
hv : MDifferentiableWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m => { proj := b₁ m, snd := v m }) univ m₀
hb₂ : MDifferentiableWithinAt IM IB₂ b₂ univ m₀
⊢ MDifferentiableWithinAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m => { proj := b₂ m, snd := (ϕ m) (v m) }) univ m₀

Proof state:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B₁) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B₂) → AddCommGroup (E₂ x)
inst✝²³ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
inst✝⁶ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ :
  MDifferentiableWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m => inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    univ m₀
hv : MDifferentiableWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m => { proj := b₁ m, snd := v m }) univ m₀
hb₂ : MDifferentiableWithinAt IM IB₂ b₂ univ m₀
⊢ MDifferentiableWithinAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m => { proj := b₂ m, snd := (ϕ m) (v m) }) univ m₀

Tactic:
exact MDifferentiableWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

Result:
no goals