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
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 :
  ContMDiffOn 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
hf : ContMDiffOn I I' n f s
hf' : ∀ x ∈ s ∩ f ⁻¹' t, IsInvertible (M := TangentSpace I x) (M₂ := TangentSpace I' (f x)) (mfderivWithin I I' f s x)
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
⊢ ContMDiffOn 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)

Tactic:
fun _ hx₀ ↦ ContMDiffWithinAt.mpullbackWithin_vectorField_inter
    (hV _ hx₀.2) (hf _ hx₀.1) (hf' _ hx₀) hx₀.1 hs hmn

Premises used: ContMDiffWithinAt.mpullbackWithin_vectorField_inter, And.right, And.left, ContMDiffOn
-- 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'
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 : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
simp :
  ∀ (hf : ContMDiffWithinAt I I' n f univ x₀)
    (hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f univ 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 univ x⟩) (f ⁻¹' t) 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, mpullback I I' f V x⟩) (f ⁻¹' t) x₀

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

Premises used: VectorField.mpullbackWithin_univ, mfderivWithin_univ, contMDiffWithinAt_univ
-- 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'
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₀)
hmn : m + 1 ≤ n
hf : ContMDiffWithinAt I I' n f univ x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f univ 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 univ x⟩) (f ⁻¹' t) x₀

Tactic:
simpa using hV.mpullbackWithin_vectorField_inter hf hf' (mem_univ _) uniqueMDiffOn_univ hmn

Premises used: ContMDiffWithinAt.mpullbackWithin_vectorField_inter, uniqueMDiffOn_univ, Set.mem_univ
-- 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'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
y₀ : 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 y₀
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hy₀ : y₀ = f x₀
⊢ 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₀)

Tactic:
subst hy₀
-- 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'
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'
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
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₀)
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t) x₀

Tactic:
ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

Premises used: ContMDiffWithinAt.mpullback_vectorField_preimage
-- 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'
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'
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
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₀)
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t) x₀

Tactic:
exact ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

Premises used: ContMDiffWithinAt.mpullback_vectorField_preimage
-- 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 : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[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, mpullback I I' f V x⟩) s x₀

Tactic:
(ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn).mono_of_mem_nhdsWithin hst

Premises used: ContMDiffWithinAt.mpullback_vectorField_preimage, ContMDiffWithinAt.mono_of_mem_nhdsWithin
-- 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'
y₀ : 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 y₀
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hy₀ : y₀ = f x₀
⊢ 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₀)

Tactic:
subst hy₀
-- 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'
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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₀)
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) s x₀

Tactic:
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin hV hf hf' hmn hst

Premises used: ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
-- 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'
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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₀)
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) s x₀

Tactic:
exact ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin hV hf hf' hmn hst

Premises used: ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
-- 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'
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 :
  ContMDiffOn 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
hf : ContMDiff I I' n f
hf' : ∀ x ∈ f ⁻¹' t, IsInvertible (M := TangentSpace I x) (M₂ := TangentSpace I' (f x)) (mfderiv% f x)
hmn : m + 1 ≤ n
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t)

Tactic:
fun x₀ hx₀ ↦ ContMDiffWithinAt.mpullback_vectorField_preimage (hV _ hx₀) (hf x₀) (hf' _ hx₀) hmn

Premises used: ContMDiffWithinAt.mpullback_vectorField_preimage, ContMDiffOn
-- 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'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffAt 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⟩) (f x₀)
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
⊢ 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⟩) univ (f x₀)

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

Premises used: contMDiffWithinAt_univ
-- 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'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffAt 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⟩) (f x₀)
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
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⟩) univ (f x₀)
⊢ ContMDiffWithinAt I I' n f univ x₀

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

Premises used: contMDiffWithinAt_univ
-- 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'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
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⟩) univ (f x₀)
hf : ContMDiffWithinAt I I' n f univ 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, mpullback I I' f V x⟩) univ x₀

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

Premises used: ContMDiffWithinAt.mpullback_vectorField_preimage
-- 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'
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiff 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⟩
hf : ContMDiff I I' n f
hf' : ∀ (x : M), IsInvertible (M := TangentSpace I x) (M₂ := TangentSpace I' (f x)) (mfderiv% f x)
hmn : m + 1 ≤ n
⊢ ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m fun (x : M) ↦
    ⟨x, mpullback I I' f V x⟩

Tactic:
fun x ↦ ContMDiffAt.mpullback_vectorField_preimage (hV (f x)) (hf x) (hf' x) hmn

Premises used: ContMDiff, ContMDiffAt.mpullback_vectorField_preimage
-- 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
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
⊢ (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s

Tactic:
simp [hx]
-- 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
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
⊢ {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x

Tactic:
have T := nhdsWithin_mono _ (subset_insert _ _)
    ((contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin hm).1
      (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx hmn))
-- 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
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
⊢ (↑(extChartAt I x) : M → E) ⁻¹'
      {x_1 : E |
        (fun (x' : E) ↦
            ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
              Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
              (fun (x_2 : E) ↦
                ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
              ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
          x_1} ∈
    𝓝[(↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)] x

Tactic:
have A := (continuousAt_extChartAt (I := I) x).continuousWithinAt.preimage_mem_nhdsWithin'' T rfl