awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
suffices :
  ContMDiffWithinAt I (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) (M' := E' →L[𝕜] E) m
    (fun (x : M) ↦ inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) s x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V s x⟩) (s ∩ f ⁻¹' t) x₀

Tactic:
suffices hϕ : CMDiffAt[s] m (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
        E' (TangentSpace I' (M := M')) E (TangentSpace I (M := M))
        (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) x₀ from
    ContMDiffWithinAt.clm_apply_of_inCoordinates (hϕ.mono inter_subset_left) hv contMDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
⊢ ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀

Tactic:
have : CMDiffAt[s] m (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
        E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M'))
        x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀ :=
    hf.mfderivWithin_const hmn hx₀ hs
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
apply :
  ContMDiffAt (E := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M := E →L[𝕜] E') (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) m inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
⊢ ContMDiffWithinAt I (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) (M' := E' →L[𝕜] E) m
    (inverse ∘ fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀

Tactic:
apply ContMDiffAt.comp_contMDiffWithinAt _ _ this

Premises used: ContMDiffAt.comp_contMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
a :
  ContDiffAt 𝕜 (E := E →L[𝕜] E') m inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
⊢ ContMDiffAt (E := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M := E →L[𝕜] E') (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) m inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))

Tactic:
apply ContDiffAt.contMDiffAt

Premises used: ContDiffAt.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
a : IsInvertible (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
⊢ ContDiffAt 𝕜 (E := E →L[𝕜] E') m inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))

Tactic:
apply IsInvertible.contDiffAt_map_inverse

Premises used: ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
a :
  IsInvertible
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀))
      (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I')
            (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯) :
        TangentSpace I' (f x₀) →L[𝕜] E')
      (ContinuousLinearMap.comp (M₂ := TangentSpace I x₀) (mfderivWithin I I' f s x₀)
        (↑(ContinuousLinearEquiv.symm
              (Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I)
                (trivializationAt E (TangentSpace I) x₀) x₀ ⋯)) :
          E →L[𝕜] TangentSpace I x₀)))
⊢ IsInvertible (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))

Tactic:
rw [inCoordinates_eq (FiberBundle.mem_baseSet_trivializationAt' x₀)
      (FiberBundle.mem_baseSet_trivializationAt' (f x₀))]

Premises used: FiberBundle.mem_baseSet_trivializationAt', ContinuousLinearMap.inCoordinates_eq
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
⊢ IsInvertible
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀))
      (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I')
            (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯) :
        TangentSpace I' (f x₀) →L[𝕜] E')
      (ContinuousLinearMap.comp (M₂ := TangentSpace I x₀) (mfderivWithin I I' f s x₀)
        (↑(ContinuousLinearEquiv.symm
              (Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I)
                (trivializationAt E (TangentSpace I) x₀) x₀ ⋯)) :
          E →L[𝕜] TangentSpace I x₀)))

Tactic:
isInvertible_equiv.comp (hf'.comp isInvertible_equiv)

Premises used: ContinuousLinearMap.isInvertible_equiv, ContinuousLinearMap.IsInvertible.comp
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
⊢ IsInvertible
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀))
      (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I')
            (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯) :
        TangentSpace I' (f x₀) →L[𝕜] E')
      (ContinuousLinearMap.comp (M₂ := TangentSpace I x₀) (mfderivWithin I I' f s x₀)
        (↑(ContinuousLinearEquiv.symm
              (Bundle.Trivialization.continuousLinearEquivAt 𝕜 (E := TangentSpace I)
                (trivializationAt E (TangentSpace I) x₀) x₀ ⋯)) :
          E →L[𝕜] TangentSpace I x₀)))

Tactic:
exact isInvertible_equiv.comp (hf'.comp isInvertible_equiv)

Premises used: ContinuousLinearMap.isInvertible_equiv, ContinuousLinearMap.IsInvertible.comp
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s
    x₀
⊢ ContMDiffWithinAt I (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) (M' := E' →L[𝕜] E) m
    (inverse ∘ fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀

Tactic:
have : CMDiffAt[s] m
      (ContinuousLinearMap.inverse ∘ (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
        E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M'))
        x₀ x (f x₀) (f x) (mfderiv[s] f x))) x₀ := by
    apply ContMDiffAt.comp_contMDiffWithinAt _ _ this
    apply ContDiffAt.contMDiffAt
    apply IsInvertible.contDiffAt_map_inverse
    rw [inCoordinates_eq (FiberBundle.mem_baseSet_trivializationAt' x₀)
      (FiberBundle.mem_baseSet_trivializationAt' (f x₀))]
    exact isInvertible_equiv.comp (hf'.comp isInvertible_equiv)
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
hv :
  ContMDiffWithinAt I I'.tangent (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M) ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this_1 :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (x : M) ↦ 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' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) (M' := E' →L[𝕜] E) m
    (inverse ∘ fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    s x₀
apply :
  (𝓝[s] x₀).EventuallyEq (β := E' →L[𝕜] E)
    (fun (x : M) ↦ inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x))
    (inverse ∘ fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
⊢ ContMDiffWithinAt I (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) (M' := E' →L[𝕜] E) m
    (fun (x : M) ↦ inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) s x₀

Tactic:
apply this.congr_of_eventuallyEq_of_mem _ hx₀

Premises used: ContMDiffWithinAt.congr_of_eventuallyEq_of_mem