Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : 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
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this✝ : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
this :
  MDiffAt[s]
      (inverse ∘ fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x))
    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
⊢ ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx) ∘SL
      ϕ x ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x)
              h'x).symm =
    (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x) ∘SL
        mfderiv[s] f x ∘SL
          ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx).symm).inverse

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

Goal state after:
𝕜 : 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
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this✝ : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
this :
  MDiffAt[s]
      (inverse ∘ fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x))
    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
⊢ ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx) ∘SL
      (mfderiv[s] f x).inverse ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x)
              h'x).symm =
    (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx) ∘SL
        (mfderiv[s] f x).inverse) ∘SL
      ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x).symm