-- Mathlib/Geometry/Manifold/VectorField.lean
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version at a point. -/
protected lemma _root_.ContMDiffAt.mpullback_vectorField_preimage
    (hV : ContMDiffAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) (f x₀))
    (hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : m + 1 ≤ n) :
    ContMDiffAt I I.tangent m
      (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hf' : (mfderiv I I' f x₀).IsInvertible
hmn : m + 1 ≤ n
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) univ (f x₀)
hf : ContMDiffWithinAt I I' n f univ x₀
⊢ ContMDiffWithinAt I I.tangent m (fun y => { proj := y, snd := mpullback I I' f V y }) univ x₀

Tactic:
simpa using ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffAt I' I'.tangent m (fun y => { proj := y, snd := V y }) (f x₀)
hf : ContMDiffAt I I' n f x₀
hf' : (mfderiv I I' f x₀).IsInvertible
hmn : m + 1 ≤ n
⊢ ContMDiffAt I I.tangent m (fun y => { proj := y, snd := mpullback I I' f V y }) x₀

Tactic:
simp only [← contMDiffWithinAt_univ] at hV hf hf' ⊢

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hf' : (mfderiv I I' f x₀).IsInvertible
hmn : m + 1 ≤ n
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) univ (f x₀)
hf : ContMDiffWithinAt I I' n f univ x₀
⊢ ContMDiffWithinAt I I.tangent m (fun y => { proj := y, snd := mpullback I I' f V y }) univ x₀