awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
hU :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, U x⟩
hV :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, V x⟩
hW :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, W x⟩
x : M
⊢ mlieBracket I U (mlieBracket I V W) x = (mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)) x

Tactic:
leibniz_identity_mlieBracket_apply (hU x) (hV x) (hW x)

Premises used: VectorField.leibniz_identity_mlieBracket_apply
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
hU :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, U x⟩
hV :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, V x⟩
hW :
  ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (x : M) ↦ ⟨x, W x⟩
x : M
⊢ mlieBracket I U (mlieBracket I V W) x = (mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)) x

Tactic:
exact leibniz_identity_mlieBracket_apply (hU x) (hV x) (hW x)

Premises used: VectorField.leibniz_identity_mlieBracket_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'
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''
f : M → M'
s t : Set M
x x₀ : M
n : ℕ
inst_16 : n.AtLeastTwo
inst_17 : IsManifold I (minSmoothness 𝕜 (OfNat.ofNat n)) M
⊢ IsManifold I (OfNat.ofNat n) M

Tactic:
IsManifold.of_le (n := minSmoothness 𝕜 n) le_minSmoothness

Premises used: le_minSmoothness, IsManifold.of_le
-- 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''
f : M → M'
s t : Set M
x x₀ : M
inst_16 : IsManifold I (minSmoothness 𝕜 1) M
⊢ IsManifold I 1 M

Tactic:
IsManifold.of_le (n := minSmoothness 𝕜 1) le_minSmoothness

Premises used: le_minSmoothness, IsManifold.of_le
-- 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''
f : M → M'
s t : Set M
x x₀ : M
inst_16 : IsManifold I (minSmoothness 𝕜 3) M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LE.le (α := ℕ) 2 3
⊢ LE.le (α := ℕ∞ω) 2 3

Tactic:
norm_cast
-- 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''
f : M → M'
s t : Set M
x x₀ : M
inst_16 : IsManifold I (minSmoothness 𝕜 2) M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LE.le (α := ℕ) 1 2
⊢ LE.le (α := ℕ∞ω) 1 2

Tactic:
norm_cast
-- 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
⊢ Eq (α := TangentSpace I x) (mpullbackWithin I I' f V s 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)
      (V (f x)))

Tactic:
rfl

Premises used: VectorField.mpullbackWithin, rfl
-- 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
c : 𝕜
⊢ mpullbackWithin I I' f (c • V) s x = HSMul.hSMul (β := TangentSpace I x) c (mpullbackWithin I I' f V s x)

Tactic:
simp [mpullbackWithin_apply]

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

Tactic:
simp [mpullbackWithin_apply]

Premises used: 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'
s : Set M
V : (x : M') → TangentSpace I' x
c : 𝕜
h :
  ∀ (x : M),
    mpullbackWithin I I' f (c • V) s x = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullbackWithin I I' f V s) x
⊢ mpullbackWithin I I' f (c • V) s = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullbackWithin I I' f V s)

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'
s : Set M
V : (x : M') → TangentSpace I' x
c : 𝕜
x : M
⊢ mpullbackWithin I I' f (c • V) s x = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullbackWithin I I' f V s) x

Tactic:
simp [mpullbackWithin_apply]

Premises used: 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'
s : Set M
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
h :
  ∀ (x : M),
    mpullbackWithin I I' f (g • V) s x =
      HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullbackWithin I I' f V s) x
⊢ mpullbackWithin I I' f (g • V) s = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullbackWithin I I' f V s)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
x : M
⊢ mpullbackWithin I I' f (g • V) s x =
    HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullbackWithin I I' f V s) x

Tactic:
simp [mpullbackWithin_apply]

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

Tactic:
simp [mpullbackWithin_apply]

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

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

Tactic:
simp [mpullbackWithin_apply]

Premises used: 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'
s : Set M
h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullbackWithin I I' f 0 s x) (0 x)
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullbackWithin I I' f 0 s) 0

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'
s : Set M
x : M
⊢ Eq (α := TangentSpace I x) (mpullbackWithin I I' f 0 s x) (0 x)

Tactic:
simp [mpullbackWithin_apply]

Premises used: 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'
s : Set M
x : M
V : (x : M') → TangentSpace I' x
⊢ Eq (α := TangentSpace I x) (mpullbackWithin I I' f (-V) s x) (-mpullbackWithin I I' f V s x)

Tactic:
simp [mpullbackWithin_apply]

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

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'
s : Set M
V : (x : M') → TangentSpace I' x
x : M
⊢ Eq (α := TangentSpace I x) (mpullbackWithin I I' f (-V) s x) ((-mpullbackWithin I I' f V s) x)

Tactic:
simp [mpullbackWithin_apply]

Premises used: 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
h : UniqueMDiffWithinAt I s x
⊢ mpullbackWithin I I id V s x = V x

Tactic:
simp [mpullbackWithin_apply, mfderivWithin_id h]

Premises used: VectorField.mpullbackWithin_apply, mfderivWithin_id
-- 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)
    (((inverse (mfderiv% f 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)
      (V (f x)))

Tactic:
rfl

Premises used: VectorField.mpullback, rfl
-- 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
c : 𝕜
⊢ mpullback I I' f (c • V) x = HSMul.hSMul (β := TangentSpace I x) c (mpullback I I' f 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'
f : M → M'
V : (x : M') → TangentSpace I' x
c : 𝕜
h : ∀ (x : M), mpullback I I' f (c • V) x = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullback I I' f V) x
⊢ mpullback I I' f (c • V) = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (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
c : 𝕜
x : M
⊢ mpullback I I' f (c • V) x = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (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
g : M' → 𝕜
⊢ mpullback I I' f (g • V) x = HSMul.hSMul (β := TangentSpace I x) (g (f x)) (mpullback I I' f 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'
f : M → M'
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
h : ∀ (x : M), mpullback I I' f (g • V) x = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullback I I' f V) x
⊢ mpullback I I' f (g • V) = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullback I I' f V)

Tactic:
ext x