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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
⊢ 1 ≤ n

Tactic:
have hn : 1 ≤ n := le_trans (by simp) 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
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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
⊢ IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)

Tactic:
hf'
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
h :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I x₀) (TangentSpace I' (f x₀)))
    (mfderivWithin I I' f s x₀) (mfderivWithin I I' f u x₀)
⊢ IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)

Tactic:
convert! hf' using 1
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
⊢ n ≠ 0

Tactic:
positivity
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I x₀) (TangentSpace I' (f x₀)))
    (mfderivWithin I I' f s x₀) (mfderivWithin I I' f u x₀)

Tactic:
exact (hf.mdifferentiableWithinAt <| by positivity).mfderivWithin_mono (hs _ hx₀) hu

Premises used: ContMDiffWithinAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mfderivWithin_mono
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
⊢ IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)

Tactic:
have hh : (mfderiv[s] f x₀).IsInvertible := by
    convert! hf' using 1
    exact (hf.mdifferentiableWithinAt <| by positivity).mfderivWithin_mono (hs _ hx₀) hu
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
apply :
  (𝓝[s] x₀).EventuallyEq (β := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V u x⟩) fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V 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 u x⟩) s x₀

Tactic:
apply (hV.mpullbackWithin_vectorField_of_mem (hf.mono hu) hh hx₀ hs hmn
    hst).congr_of_eventuallyEq_of_mem _ hx₀

Premises used: ContMDiffWithinAt.mono, ContMDiffWithinAt.congr_of_eventuallyEq_of_mem, ContMDiffWithinAt.mpullbackWithin_vectorField_of_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
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ Ne (α := ℕ∞ω) 1 ∞

Tactic:
simp
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ ∀ᶠ (x' : M) in 𝓝[insert x₀ u] x₀, ContMDiffWithinAt I I' 1 f u x'

Tactic:
have Y := (contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin (by simp)).1 (hf.of_le hn)
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
Y : ∀ᶠ (x' : M) in 𝓝[insert x₀ u] x₀, ContMDiffWithinAt I I' 1 f u x'
⊢ ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'

Tactic:
simp_rw [insert_eq_of_mem (hu hx₀)] at Y

Premises used: Set.insert_eq_of_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
m n : ℕ∞ω
t : Set M'
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
h :
  ∀ (y : M) (hy : y ∈ s) (h'y : ContMDiffWithinAt I I' 1 f u y),
    Eq (α := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) ⟨y, mpullbackWithin I I' f V u y⟩
      ⟨y, mpullbackWithin I I' f V s y⟩
⊢ (𝓝[s] x₀).EventuallyEq (β := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V u x⟩) fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V s x⟩

Tactic:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_mono _ hu Y] with y hy h'y

Premises used: self_mem_nhdsWithin, nhdsWithin_mono
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
y : M
hy : y ∈ s
h'y : ContMDiffWithinAt I I' 1 f u y
h :
  Eq.{u_3 + 1} (α := TangentSpace I y)
    (((inverse (mfderivWithin I I' f u y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
    (((inverse (mfderivWithin I I' f s y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
⊢ Eq (α := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) ⟨y, mpullbackWithin I I' f V u y⟩
    ⟨y, mpullbackWithin I I' f V s y⟩

Tactic:
simp only [mpullbackWithin, Bundle.TotalSpace.mk_inj]

Premises used: VectorField.mpullbackWithin, Bundle.TotalSpace.mk_inj
-- 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'
u : Set 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 u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
y : M
hy : y ∈ s
h'y : ContMDiffWithinAt I I' 1 f u y
h h₁ :
  Eq.{u_3 + 1} (α := TangentSpace I y)
    (((inverse (mfderivWithin I I' f u y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
    (((inverse (mfderivWithin I I' f u y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
⊢ Eq.{u_3 + 1} (α := TangentSpace I y)
    (((inverse (mfderivWithin I I' f u y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
    (((inverse (mfderivWithin I I' f s y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)

Tactic:
rw [MDifferentiableWithinAt.mfderivWithin_mono (h'y.mdifferentiableWithinAt one_ne_zero)
    (hs _ hy) hu]

Premises used: ContMDiffWithinAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mfderivWithin_mono, one_ne_zero
-- 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'
u : Set 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 : ContMDiffWithinAt I I' n f u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hy₀ : f x₀ = y₀
⊢ 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'
u : Set M
hf : ContMDiffWithinAt I I' n f u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
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, mpullbackWithin I I' f V u x⟩) s x₀

Tactic:
ContMDiffWithinAt.mpullbackWithin_vectorField' hV hf hf' hx₀ hs hmn hst hu

Premises used: ContMDiffWithinAt.mpullbackWithin_vectorField'
-- 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'
u : Set M
hf : ContMDiffWithinAt I I' n f u x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f u x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
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, mpullbackWithin I I' f V u x⟩) s x₀

Tactic:
exact ContMDiffWithinAt.mpullbackWithin_vectorField' hV hf hf' hx₀ hs hmn hst hu

Premises used: ContMDiffWithinAt.mpullbackWithin_vectorField'