-- Mathlib/Geometry/Manifold/VectorField.lean
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
`m + 1 ≤ n` is `C^m`.
Version within a set at a point. -/
protected lemma _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_inter
    (hV : ContMDiffWithinAt I' I'.tangent m
      (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
    (hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible)
    (hx₀ : x₀ ∈ s) (hs : UniqueMDiffOn I s) (hmn : m + 1 ≤ n) :
    ContMDiffWithinAt I I.tangent m
      (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t) x₀

Proof state:
case h
𝕜 : 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'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : ContMDiffWithinAt I I'.tangent m (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
this✝ :
  ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
    (fun x => inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s x₀
this :
  ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
    (inverse ∘ fun x =>
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀
A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀
B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (trivializationAt E (TangentSpace I) x₀).baseSet
h'x : x ∈ f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet
⊢ (↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx)).comp
      ((mfderivWithin I I' f s x).inverse.comp
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x) h'x).symm) =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx)).comp
          (mfderivWithin I I' f s x).inverse).comp
      ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x).symm

Tactic:
rfl

Result:
no goals

Proof state:
case h
𝕜 : 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'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : ContMDiffWithinAt I I'.tangent m (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
this✝ :
  ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
    (fun x => inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s x₀
this :
  ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
    (inverse ∘ fun x =>
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀
A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀
B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (trivializationAt E (TangentSpace I) x₀).baseSet
h'x : x ∈ f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet
⊢ (↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx)).comp
      ((ϕ x).comp
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x) h'x).symm) =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x)).comp
        ((mfderivWithin I I' f s x).comp
          ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx).symm)).inverse

Tactic:
simp only [inverse_equiv_comp, inverse_comp_equiv, ContinuousLinearEquiv.symm_symm, ϕ]

Result:
case h
𝕜 : 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'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : ContMDiffWithinAt I I'.tangent m (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
this✝ :
  ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
    (fun x => inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s x₀
this :
  ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
    (inverse ∘ fun x =>
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀
A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀
B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (trivializationAt E (TangentSpace I) x₀).baseSet
h'x : x ∈ f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet
⊢ (↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx)).comp
      ((mfderivWithin I I' f s x).inverse.comp
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x) h'x).symm) =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx)).comp
          (mfderivWithin I I' f s x).inverse).comp
      ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x).symm