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
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₀)
⊢ IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
have this : (↑(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)
Tactic: have : ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target : Set E)
      =ᶠ[𝓝 (extChartAt I x₀ x₀)] ((extChartAt I x₀).symm ⁻¹' s ∩ range I : Set E) :=
    EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq
-- 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 :
  (↑(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)
⊢ IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
have apply : 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₀)
Tactic: apply IsSymmSndFDerivWithinAt.congr_set _ 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 :
  (↑(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)
⊢ 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₀)
have hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
Tactic: apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
-- 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 :
  (↑(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)
hs₁ : 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) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
have hx : (↑(extChartAt I x₀) : M → E) x₀ ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target))
Tactic: apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
-- 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 :
  (↑(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)
hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
hx :
  (↑(extChartAt I x₀) : M → E) x₀ ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (interior ((↑(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) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
have h'x : (↑(extChartAt I x₀) : M → E) x₀ ∈ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target
Tactic: apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
-- 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 :
  (↑(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)
hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
hx :
  (↑(extChartAt I x₀) : M → E) x₀ ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target))
h'x : (↑(extChartAt I x₀) : M → E) x₀ ∈ (↑(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) ⁻¹' u ∩ (extChartAt I x₀).target) ((↑(extChartAt I x₀) : M → E) x₀)
have apply : ContDiffWithinAt 𝕜 (minSmoothness 𝕜 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₀)
Tactic: apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
-- 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 :
  (↑(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)
⊢ UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)
have hs₁ : 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 (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 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 :
  (↑(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)
⊢ 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 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₀)
Tactic: have : IsSymmSndFDerivWithinAt 𝕜 ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
      ((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) := by
    apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
    · rw [inter_comm]
      exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀
    · apply extChartAt_mem_closure_interior h'x₀ (mem_extChartAt_source x₀)
    · simp [hsu hx₀]
    · exact B.of_le hn
-- 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₀)
⊢ 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 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₀
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₀
⊢ 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 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₀)
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₀)
⊢ 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 hs₁ : UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target)
Tactic: apply IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin this