awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiffOn I s
hu : UniqueMDiffOn I u
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst_4] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
this_1 :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
this :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
hst₁ :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target ∈
    𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target] (↑(extChartAt I x₀) : M → E) x₀
hf₁ :
  ContDiffWithinAt 𝕜 2 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target)
⊢ IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
have ht : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
Tactic: apply IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin this
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiffOn I s
hu : UniqueMDiffOn I u
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst_4] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
this_1 :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
this :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
hst₁ :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target ∈
    𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target] (↑(extChartAt I x₀) : M → E) x₀
hf₁ :
  ContDiffWithinAt 𝕜 2 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target)
ht : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
⊢ IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
have hx : (↑(extChartAt I x₀) : M → E) x₀ ∈ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target
Tactic: apply IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin this
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiffOn I s
hu : UniqueMDiffOn I u
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst_4] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
this_1 :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
this :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target)
have hs₁ : UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s)
Tactic: rw [inter_comm]
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiffOn I s
hu : UniqueMDiffOn I u
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst_4] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
this_1 :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
this :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
have ht : UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u)
Tactic: rw [inter_comm]
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((ContinuousLinearMap.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₀)
        (mlieBracketWithin I' V W t (f x₀)) :
      TangentSpace I x₀)
    (((ContinuousLinearMap.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₀)
        (mlieBracketWithin I' V W t (f x₀)) :
      TangentSpace I x₀)
have e_a : Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I x₀) (TangentSpace I' (f x₀)))
  (mfderiv% f x₀) (mfderivWithin I I' f s x₀)
Tactic: congr
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I x₀) (TangentSpace I' (f x₀)))
    (mfderiv% f x₀) (mfderivWithin I I' f s x₀)
have apply : MDiffAt f x₀
Tactic: apply (mfderivWithin_eq_mfderiv (hu _ hx₀) _).symm
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
⊢ Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀)
have this : Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
  (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
Tactic: have : mpullback I I' f (mlieBracketWithin I' V W t) x₀ =
      mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ := by
    simp only [mpullback, mpullbackWithin]
    congr
    apply (mfderivWithin_eq_mfderiv (hu _ hx₀) _).symm
    exact hf.mdifferentiableAt (two_pos.trans_le (le_minSmoothness.trans hn)).ne'
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
⊢ Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀)
have rw : Eq (α := TangentSpace I x₀) (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)
  (mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀)
Tactic: rw [this, mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt
    hx₀ hn hst (by simp) (subset_univ _)]
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
⊢ Eq (α := TangentSpace I x₀) (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)
    (mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀)
have hV₁ : mpullbackWithin I I' f V s =ᶠ[𝓝[insert x₀ s] x₀] mpullback I I' f V
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
hV₁ : mpullbackWithin I I' f V s =ᶠ[𝓝[insert x₀ s] x₀] mpullback I I' f V
⊢ Eq (α := TangentSpace I x₀) (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)
    (mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀)
have hW₁ : mpullbackWithin I I' f W s =ᶠ[𝓝[insert x₀ s] x₀] mpullback I I' f W
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
⊢ mpullbackWithin I I' f V s =ᶠ[𝓝[insert x₀ s] x₀] mpullback I I' f V
have hV₁ : mpullbackWithin I I' f V s =ᶠ[𝓝[s] x₀] mpullback I I' f V
Tactic: rw [insert_eq_of_mem hx₀]
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
⊢ mpullbackWithin I I' f V s =ᶠ[𝓝[s] x₀] mpullback I I' f V
have h : ∀ (y : M) (hy : ContMDiffAt I I' 2 f y) (h'y : y ∈ s),
  Eq (α := E) (mpullbackWithin I I' f V s y : TangentSpace I y) (mpullback I I' f V y)
Tactic: filter_upwards [nhdsWithin_le_nhds ((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1
      (hf.of_le (le_minSmoothness.trans hn))), self_mem_nhdsWithin] with y hy h'y
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
y : M
hy : ContMDiffAt I I' 2 f y
h'y : y ∈ s
⊢ Eq.{u_3 + 1} (α := E)
    (((ContinuousLinearMap.inverse (mfderivWithin I I' f s y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
    (((ContinuousLinearMap.inverse (mfderiv% f y) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f y)) (TangentSpace I y)) :
          (a : TangentSpace I' (f y)) → TangentSpace I y)
        (V (f y)) :
      TangentSpace I y)
have h : Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I y) (TangentSpace I' (f y)))
  (mfderivWithin I I' f s y) (mfderiv% f y)
Tactic: congr
-- 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
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'
inst_11 : IsManifold I (minSmoothness 𝕜 2) M
inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'
inst_13 : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this :
  Eq (α := TangentSpace I x₀) (mpullback I I' f (mlieBracketWithin I' V W t) x₀)
    (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
y : M
hy : ContMDiffAt I I' 2 f y
h'y : y ∈ s
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I y) (TangentSpace I' (f y)))
    (mfderivWithin I I' f s y) (mfderiv% f y)
have h : MDiffAt f y
Tactic: apply mfderivWithin_eq_mfderiv (hu _ h'y)