awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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
⊢ 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₀
have hn : 1 ≤ n
Tactic: have hn : 1 ≤ n := le_trans (by simp) hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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₀)
have 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₀)
Tactic: convert! hf' using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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
⊢ 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₀
have hh : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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₀)
⊢ 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₀
have 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⟩
Tactic: apply (hV.mpullbackWithin_vectorField_of_mem (hf.mono hu) hh hx₀ hs hmn
    hst).congr_of_eventuallyEq_of_mem _ hx₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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₀)
⊢ (𝓝[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⟩
have Y : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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'
⊢ (𝓝[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⟩
have Y₁ : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
Tactic: simp_rw [insert_eq_of_mem (hu hx₀)] at Y
Cleared hypotheses: Y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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'
⊢ (𝓝[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⟩
have 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⟩
Tactic: filter_upwards [self_mem_nhdsWithin, nhdsWithin_mono _ hu Y] with y hy h'y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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
⊢ 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⟩
have 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)
Tactic: simp only [mpullbackWithin, Bundle.TotalSpace.mk_inj]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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
⊢ 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)
have 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)
Tactic: rw [MDifferentiableWithinAt.mfderivWithin_mono (h'y.mdifferentiableWithinAt one_ne_zero)
    (hs _ hy) hu]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V u x⟩) s x₀
have 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₀)
Tactic: subst hy₀
Cleared hypotheses: y₀, hV, hy₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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
⊢ 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₀
have 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₀
Tactic: simp only [← contMDiffWithinAt_univ, ← mfderivWithin_univ, ← mpullbackWithin_univ] at hV hf hf' ⊢
Cleared hypotheses: hf, hf'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t) x₀
have 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₀)
Tactic: subst hy₀
Cleared hypotheses: y₀, hV, hy₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) s x₀
have 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₀)
Tactic: subst hy₀
Cleared hypotheses: y₀, hV, hy₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (hypothesis)
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
⊢ ContMDiffAt 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⟩) x₀
have 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₀)
Tactic: simp only [← contMDiffWithinAt_univ] at hV hf hf' ⊢
Cleared hypotheses: hV, hf