awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiffOn I s
h's : x ∈ closure[inst_4] (interior s)
hx : x ∈ s
hU :
  ContMDiffWithinAt 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⟩) s x
hV :
  ContMDiffWithinAt 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⟩) s x
hW :
  ContMDiffWithinAt 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⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
pre_mem : (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) U (range (↑I : H → E))
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
⊢ mlieBracketWithin I U (mlieBracketWithin I V W s) s x =
    mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x
have J0V : ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
  Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, V' x⟩)
  ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
Tactic: have J0V : CMDiffAt[(extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s] (minSmoothness 𝕜 2)
      (T% V') (extChartAt I x x) :=
    contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiffOn I s
h's : x ∈ closure[inst_4] (interior s)
hx : x ∈ s
hU :
  ContMDiffWithinAt 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⟩) s x
hV :
  ContMDiffWithinAt 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⟩) s x
hW :
  ContMDiffWithinAt 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⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
pre_mem : (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) U (range (↑I : H → E))
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
J0V :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, V' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
⊢ mlieBracketWithin I U (mlieBracketWithin I V W s) s x =
    mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x
have J0W : ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
  Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, W' x⟩)
  ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
Tactic: have J0W : CMDiffAt[(extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s] (minSmoothness 𝕜 2)
      (T% W') (extChartAt I x x) :=
    contMDiffWithinAt_mpullbackWithin_extChartAt_symm hW hs hx A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
x : M
hU :
  ContMDiffAt 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⟩) x
hV :
  ContMDiffAt 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⟩) x
hW :
  ContMDiffAt 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
⊢ mlieBracket I U (mlieBracket I V W) x = mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x
have simp : ∀
  (hU :
    ContMDiffWithinAt 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⟩) univ x)
  (hV :
    ContMDiffWithinAt 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⟩) univ x)
  (hW :
    ContMDiffWithinAt 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⟩) univ x),
  mlieBracketWithin I U (mlieBracketWithin I V W univ) univ x =
    mlieBracketWithin I (mlieBracketWithin I U V univ) W univ x +
      mlieBracketWithin I V (mlieBracketWithin I U W univ) univ x
Tactic: simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hU hV hW ⊢
Cleared hypotheses: hU, hV, hW
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (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
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⟩
⊢ mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)
have h : ∀ (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: ext x
-- 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''
f : M → M'
s t : Set M
x x₀ : M
inst_16 : IsManifold I (minSmoothness 𝕜 3) M
⊢ LE.le (α := ℕ∞ω) 2 3
have norm_cast : LE.le (α := ℕ) 2 3
Tactic: norm_cast
-- 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''
f : M → M'
s t : Set M
x x₀ : M
inst_16 : IsManifold I (minSmoothness 𝕜 2) M
⊢ LE.le (α := ℕ∞ω) 1 2
have norm_cast : LE.le (α := ℕ) 1 2
Tactic: norm_cast
-- 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
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullbackWithin I I' f (c • V) s = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullbackWithin I I' f V s)
have 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
Tactic: ext x
-- 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
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
⊢ mpullbackWithin I I' f (g • V) s = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullbackWithin I I' f V s)
have 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
Tactic: ext
-- 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
V V₁ : (x : M') → TangentSpace I' 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)
have 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
Tactic: ext x
-- 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
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullbackWithin I I' f 0 s) 0
have h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullbackWithin I I' f 0 s x) (0 x)
Tactic: ext x
-- 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
V : (x : M') → TangentSpace I' x
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullbackWithin I I' f (-V) s) (-mpullbackWithin I I' f V s)
have h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullbackWithin I I' f (-V) s x) ((-mpullbackWithin I I' f V s) x)
Tactic: ext x
-- 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'
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullback I I' f (c • V) = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullback I I' f V)
have h : ∀ (x : M), mpullback I I' f (c • V) x = HSMul.hSMul (β := (x : M) → TangentSpace I x) c (mpullback I I' f V) x
Tactic: ext x
-- 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'
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
⊢ mpullback I I' f (g • V) = HSMul.hSMul (β := (x : M) → TangentSpace I x) (g ∘ f) (mpullback I I' f V)
have 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
Tactic: ext x
-- 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'
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (V + V₁) = HAdd.hAdd (α := (x : M) → TangentSpace I x) (mpullback I I' f V) (mpullback I I' f V₁)
have 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
Tactic: ext x
-- 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'
V : (x : M') → TangentSpace I' x
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullback I I' f (-V)) (-mpullback I I' f V)
have h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullback I I' f (-V) x) ((-mpullback I I' f V) x)
Tactic: ext x
-- 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'
V : (x : M') → TangentSpace I' x
⊢ Eq (α := (x : M) → TangentSpace I x) (mpullbackWithin I I' f V univ) (mpullback I I' f V)
have h : ∀ (x : M), Eq (α := TangentSpace I x) (mpullbackWithin I I' f V univ x) (mpullback I I' f V x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s
have h : ∀ (x : E), mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
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
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x
have 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)
Tactic: simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin]
-- 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
V : (x : M) → TangentSpace I x
⊢ mpullback I I id V = V
have h : ∀ (x : M), mpullback I I id V x = V x
Tactic: ext x
-- 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₀))
⊢ 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]