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'
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
x : M
⊢ mpullback I I' f (g • V) x = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullback I I' f V) x

Tactic:
simp [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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 V₁ : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (V + V₁) x = HAdd.hAdd (α := TangentSpace I x) (mpullback I I' f V x) (mpullback I I' f V₁ x)

Tactic:
simp [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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 V₁ : (x : M') → TangentSpace I' x
h :
  ∀ (x : M),
    mpullback I I' f (V + V₁) x =
      HAdd.hAdd (α := (x : M) → TangentSpace I x) (β := (x : M) → TangentSpace I x) (mpullback I I' f V)
        (mpullback I I' f V₁) x
⊢ mpullback I I' f (V + V₁) = HAdd.hAdd (α := (x : M) → TangentSpace I x) (mpullback I I' f V) (mpullback I I' f V₁)

Tactic:
ext x
-- 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 V₁ : (x : M') → TangentSpace I' x
x : M
⊢ mpullback I I' f (V + V₁) x =
    HAdd.hAdd (α := (x : M) → TangentSpace I x) (β := (x : M) → TangentSpace I x) (mpullback I I' f V)
      (mpullback I I' f V₁) x

Tactic:
simp [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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
⊢ Eq (α := TangentSpace I x) (mpullback I I' f (-V) x) (-mpullback I I' f V x)

Tactic:
simp [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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
h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullback I I' f (-V) x) ((-mpullback I I' f V) x)
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullback I I' f (-V)) (-mpullback I I' f V)

Tactic:
ext x
-- 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
x : M
⊢ Eq (α := TangentSpace I x) (mpullback I I' f (-V) x) ((-mpullback I I' f V) x)

Tactic:
simp [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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
h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullbackWithin I I' f V univ x) (mpullback I I' f V x)
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullbackWithin I I' f V univ) (mpullback I I' f V)

Tactic:
ext x
-- 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
x : M
⊢ Eq (α := TangentSpace I x) (mpullbackWithin I I' f V univ x) (mpullback I I' f V x)

Tactic:
simp [mpullback_apply, mpullbackWithin_apply]

Premises used: VectorField.mpullback_apply, VectorField.mpullbackWithin_apply
-- 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'
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullback I I' f 0) 0

Tactic:
simp [← mpullbackWithin_univ]

Premises used: VectorField.mpullbackWithin_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_6
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
h : ∀ (x : E), mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_6
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
h :
  Eq.{u_3 + 1} (α := TangentSpace 𝓘(𝕜, E) x)
    (((inverse (fderivWithin 𝕜 f s x) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E') (f x))
              (TangentSpace 𝓘(𝕜, E) x)) :
          (a : TangentSpace 𝓘(𝕜, E') (f x)) → TangentSpace 𝓘(𝕜, E) x)
        (V (f x)) :
      TangentSpace 𝓘(𝕜, E) x)
    ((inverse (fderivWithin 𝕜 f s x) : (a : E') → E) (V (f x)) : E)
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x

Tactic:
simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin]

Premises used: VectorField.mpullbackWithin, VectorField.pullbackWithin, mfderivWithin_eq_fderivWithin
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_6
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ Eq.{u_3 + 1} (α := TangentSpace 𝓘(𝕜, E) x)
    (((inverse (fderivWithin 𝕜 f s x) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E') (f x))
              (TangentSpace 𝓘(𝕜, E) x)) :
          (a : TangentSpace 𝓘(𝕜, E') (f x)) → TangentSpace 𝓘(𝕜, E) x)
        (V (f x)) :
      TangentSpace 𝓘(𝕜, E) x)
    ((inverse (fderivWithin 𝕜 f s x) : (a : E') → E) (V (f x)) : E)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_6
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
⊢ mpullback 𝓘(𝕜, E) 𝓘(𝕜, E') f V = pullback 𝕜 f V

Tactic:
simp only [← mpullbackWithin_univ, ← pullbackWithin_univ, mpullbackWithin_eq_pullbackWithin]

Premises used: VectorField.mpullbackWithin_univ, VectorField.pullbackWithin_univ, VectorField.mpullbackWithin_eq_pullbackWithin
-- 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
V : (x : M) → TangentSpace I x
h : ∀ (x : M), mpullback I I id V x = V x
⊢ mpullback I I id V = V

Tactic:
ext x
-- 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
V : (x : M) → TangentSpace I x
x : M
⊢ mpullback I I id V x = V x

Tactic:
simp [mpullback]

Premises used: VectorField.mpullback
-- 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'
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₀))
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₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I'' (g ∘ f) V s x₀)
    (mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀)

Tactic:
simp only [mpullbackWithin]

Premises used: VectorField.mpullbackWithin
-- 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'
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₀))
⊢ MDiffAt[t] g (f x₀)

Tactic:
have hg : MDifferentiableWithinAt I' I'' g t (f x₀) :=
    mdifferentiableWithinAt_of_isInvertible_mfderivWithin hg'
-- 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'
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₀)
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₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I'' (g ∘ f) V s x₀)
    (mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀)

Tactic:
simp only [mpullbackWithin]

Premises used: VectorField.mpullbackWithin
-- 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'
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₀)
⊢ MDiffAt[s] f x₀

Tactic:
have hf : MDifferentiableWithinAt I I' f s x₀ :=
    mdifferentiableWithinAt_of_isInvertible_mfderivWithin 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
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)
⊢ 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
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)
apply : s ∩ f ⁻¹' t ⊆ f ⁻¹' t
⊢ (MDiffAt[s ∩ f ⁻¹' t] fun (x : M) ↦ ⟨f x, v x⟩) x₀

Tactic:
apply hV.comp x₀ ((hf.mdifferentiableWithinAt (by positivity)).mono inter_subset_left)

Premises used: Set.inter_subset_left, MDifferentiableWithinAt.mono, MDifferentiableWithinAt.comp, ContMDiffWithinAt.mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
⊢ s ∩ f ⁻¹' t ⊆ f ⁻¹' t

Tactic:
MapsTo.mono_left (mapsTo_preimage _ _) inter_subset_right

Premises used: Set.Mem, Set.Subset, Set.mapsTo_preimage, Set.MapsTo.mono_left, Set.MapsTo, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I x) :=
  fun (x : M) ↦ inverse (mfderivWithin I I' f s x)
⊢ s ∩ f ⁻¹' t ⊆ f ⁻¹' t

Tactic:
exact MapsTo.mono_left (mapsTo_preimage _ _) inter_subset_right

Premises used: Set.mapsTo_preimage, Set.MapsTo.mono_left, Set.inter_subset_right