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'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDiffAt[s] f x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : IsInvertible (M := TangentSpace I' (f x₀)) (M₂ := TangentSpace I'' (g (f x₀))) (mfderivWithin I' I'' g t (f x₀))
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
have hg : MDiffAt[t] g (f x₀)
Tactic: have hg : MDifferentiableWithinAt I' I'' g t (f x₀) :=
    mdifferentiableWithinAt_of_isInvertible_mfderivWithin hg'
-- 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'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDiffAt[s] f x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : IsInvertible (M := TangentSpace I' (f x₀)) (M₂ := TangentSpace I'' (g (f x₀))) (mfderivWithin I' I'' g t (f x₀))
hg : MDiffAt[t] g (f x₀)
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
have rw : Eq.{u_3 + 1} (α := TangentSpace I x₀)
  (((inverse
            (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I' I'' g t (f x₀))
              (mfderivWithin I I' f s x₀)) :
          ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
      (V ((g ∘ f) x₀)) :
    TangentSpace I x₀)
  (((inverse (mfderivWithin I I' f s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
      (((inverse (mfderivWithin I' I'' g t (f x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
              (TangentSpace I' (f x₀))) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
        (V (g (f x₀)))) :
    TangentSpace I x₀)
Tactic: rw [mfderivWithin_comp _ hg hf h hu, Function.comp_apply,
    IsInvertible.inverse_comp_apply_of_left hg']
-- 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'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I'' (g ∘ f) V s x₀)
    (mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀)
have simp : Eq.{u_3 + 1} (α := TangentSpace I x₀)
  (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
      (V ((g ∘ f) x₀)) :
    TangentSpace I x₀)
  (((inverse (mfderivWithin I I' f s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
      (((inverse (mfderivWithin I' I'' g t (f x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
              (TangentSpace I' (f x₀))) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
        (V (g (f x₀)))) :
    TangentSpace I x₀)
Tactic: simp only [mpullbackWithin]
-- 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'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
have hf : MDiffAt[s] f x₀
Tactic: have hf : MDifferentiableWithinAt I I' f s x₀ :=
    mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf'
-- 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'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hf : MDiffAt[s] f x₀
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
have rw : Eq.{u_3 + 1} (α := TangentSpace I x₀)
  (((inverse
            (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I' I'' g t (f x₀))
              (mfderivWithin I I' f s x₀)) :
          ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
      (V ((g ∘ f) x₀)) :
    TangentSpace I x₀)
  (((inverse (mfderivWithin I I' f s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
      (((inverse (mfderivWithin I' I'' g t (f x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
              (TangentSpace I' (f x₀))) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
        (V (g (f x₀)))) :
    TangentSpace I x₀)
Tactic: rw [mfderivWithin_comp _ hg hf h hu, IsInvertible.inverse_comp_apply_of_right hf',
    Function.comp_apply]
-- 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
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)
⊢ (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
have apply : s ∩ f ⁻¹' t ⊆ f ⁻¹' t
Tactic: apply hV.comp x₀ ((hf.mdifferentiableWithinAt (by positivity)).mono inter_subset_left)
-- 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
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)
⊢ (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V s x⟩) x₀
have hv : (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀
Tactic: have hv : MDifferentiableWithinAt I I'.tangent
      (fun x ↦ (v x : TangentBundle I' M')) (s ∩ f ⁻¹' t) x₀ := by
    apply hV.comp x₀ ((hf.mdifferentiableWithinAt (by positivity)).mono inter_subset_left)
    exact MapsTo.mono_left (mapsTo_preimage _ _) inter_subset_right
-- 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
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₀
⊢ (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨x, mpullbackWithin I I' f V s x⟩) x₀
have suffices : (MDiffAt[s] fun (x : M) ↦ inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) x₀
Tactic: suffices hϕ : MDifferentiableWithinAt I 𝓘(𝕜, E' →L[𝕜] E)
      (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
        E' (TangentSpace I' (M := M')) E (TangentSpace I (M := M))
        (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) s x₀ from
    MDifferentiableWithinAt.clm_apply_of_inCoordinates (hϕ.mono inter_subset_left)
      hv mdifferentiableWithinAt_id
-- 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
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₀
⊢ (MDiffAt[s] fun (x : M) ↦ inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x))
    x₀
have this : (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₀
Tactic: have : MDifferentiableWithinAt I 𝓘(𝕜, E →L[𝕜] E')
      (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
        E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M'))
        x₀ x (f x₀) (f x) (mfderiv[s] f x)) s x₀ :=
    ((hf.of_le hmn).mfderivWithin_const le_rfl hx₀ hs).mdifferentiableWithinAt one_ne_zero
-- 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
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 :
  (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₀
⊢ 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₀
have apply : MDiffAt inverse (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
Tactic: apply MDifferentiableAt.comp_mdifferentiableWithinAt _ _ this
-- 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
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 :
  (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₀
⊢ MDiffAt inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
have apply : ContMDiffAt (E := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M := E →L[𝕜] E') (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) 1 inverse
  (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
Tactic: apply ContMDiffAt.mdifferentiableAt _ one_ne_zero
-- 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
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 :
  (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₀
⊢ ContMDiffAt (E := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M := E →L[𝕜] E') (E' := E' →L[𝕜] E) 𝓘(𝕜, E' →L[𝕜] E) 1 inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
have a : ContDiffAt 𝕜 (E := E →L[𝕜] E') 1 inverse
  (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀))
Tactic: apply ContDiffAt.contMDiffAt