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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
a :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝 x₀
⊢ Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
a :
  x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀)
⊢ Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝 x₀

Tactic:
apply (trivializationAt _ _ _).open_baseSet.mem_nhds

Premises used: Bundle.Trivialization.open_baseSet, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
⊢ x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀)

Tactic:
FiberBundle.mem_baseSet_trivializationAt' _

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
⊢ x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀)

Tactic:
exact FiberBundle.mem_baseSet_trivializationAt' _

Premises used: FiberBundle.mem_baseSet_trivializationAt'
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
⊢ Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀

Tactic:
have A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀ := by
    apply nhdsWithin_le_nhds
    apply (trivializationAt _ _ _).open_baseSet.mem_nhds
    exact FiberBundle.mem_baseSet_trivializationAt' _
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
apply :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
      (trivializationAt E' (TangentSpace I') (f x₀)) ∈
    𝓝 (f x₀)
⊢ f ⁻¹'
      Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
        (trivializationAt E' (TangentSpace I') (f x₀)) ∈
    𝓝[s] x₀

Tactic:
apply hf.continuousWithinAt.preimage_mem_nhdsWithin

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin, ContMDiffWithinAt.continuousWithinAt
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
apply :
  f x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
      (trivializationAt E' (TangentSpace I') (f x₀))
⊢ Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
      (trivializationAt E' (TangentSpace I') (f x₀)) ∈
    𝓝 (f x₀)

Tactic:
apply (trivializationAt _ _ _).open_baseSet.mem_nhds

Premises used: Bundle.Trivialization.open_baseSet, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
⊢ f x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
      (trivializationAt E' (TangentSpace I') (f x₀))

Tactic:
FiberBundle.mem_baseSet_trivializationAt' _

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
⊢ f x₀ ∈
    Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
      (trivializationAt E' (TangentSpace I') (f x₀))

Tactic:
exact FiberBundle.mem_baseSet_trivializationAt' _

Premises used: FiberBundle.mem_baseSet_trivializationAt'
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
⊢ f ⁻¹'
      Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
        (trivializationAt E' (TangentSpace I') (f x₀)) ∈
    𝓝[s] x₀

Tactic:
have B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀ := by
    apply hf.continuousWithinAt.preimage_mem_nhdsWithin
    apply (trivializationAt _ _ _).open_baseSet.mem_nhds
    exact FiberBundle.mem_baseSet_trivializationAt' _
-- 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
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (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 : 2 ≤ 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 : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
this_1 :
  (MDiffAt[s] fun (x : M) ↦
      inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
this :
  MDiffAt[s]
      (inverse ∘ fun (x : M) ↦
        inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x))
    x₀
A :
  Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x₀) ∈
    𝓝[s] x₀
B :
  f ⁻¹'
      Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
        (trivializationAt E' (TangentSpace I') (f x₀)) ∈
    𝓝[s] x₀
h :
  ∀ (x : M)
    (hx :
      x ∈
        Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
          (trivializationAt E (TangentSpace I) x₀))
    (h'x :
      x ∈
        f ⁻¹'
          Bundle.Trivialization.baseSet (Z := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I'))
            (trivializationAt E' (TangentSpace I') (f x₀))),
    Eq (α := E' →L[𝕜] E) (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))
        x)
⊢ (𝓝[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))

Tactic:
filter_upwards [A, B] with x hx h'x