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
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 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  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₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
s'_eq : s' =ᶠ[𝓝 x₀] s
t' : Set M' := t ∩ (extChartAt I' (f x₀)).source
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
y : M
hy :
  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) (mfderivWithin I I' f s y)
⊢ Eq (α := E) (mpullbackWithin I I' f W s' y : TangentSpace I y) (mpullbackWithin I I' f W s y)

Tactic:
simp [mpullbackWithin, hy]

Premises used: VectorField.mpullbackWithin
-- 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
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 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  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₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
s'_eq : s' =ᶠ[𝓝 x₀] s
t' : Set M' := t ∩ (extChartAt I' (f x₀)).source
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
h :
  ∀ (a : M),
    Membership.mem (γ := Set M)
      {x : M |
        Membership.mem (γ := Set M)
            {x : M |
              (fun (y : M) ↦
                  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) (mfderivWithin I I' f s y))
                x}
            x →
          Membership.mem (γ := Set M)
            {x : M |
              (fun (x : M) ↦
                  Eq (α := E) (mpullbackWithin I I' f W s' x : TangentSpace I x) (mpullbackWithin I I' f W s x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (y : M)
    (hy :
      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) (mfderivWithin I I' f s y)),
    Eq (α := E) (mpullbackWithin I I' f W s' y : TangentSpace I y) (mpullbackWithin I I' f W s y)
⊢ {x : M |
      (fun (x : M) ↦ Eq (α := E) (mpullbackWithin I I' f W s' x : TangentSpace I x) (mpullbackWithin I I' f W s x)) x} ∈
    𝓝 x₀

Tactic:
filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, hy]

Premises used: mfderivWithin_eventually_congr_set
-- 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
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
apply :
  (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target
⊢ 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₀)

Tactic:
apply (contMDiffWithinAt_iff.1 hf).2.congr_set

Premises used: ContDiffWithinAt.congr_set, contMDiffWithinAt_iff, And.right, Iff.mp
-- 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
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
⊢ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' u

Tactic:
rfl
-- 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
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
⊢ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target

Tactic:
exact EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq.symm

Premises used: extChartAt_target_eventuallyEq, Filter.EventuallyEq.inter, Filter.EventuallyEq.symm
-- 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
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
⊢ 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₀)

Tactic:
have B : ContDiffWithinAt 𝕜 n ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
      ((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) := by
    apply (contMDiffWithinAt_iff.1 hf).2.congr_set
    exact EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq.symm
-- 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
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₀)
apply :
  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₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
    (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)

Tactic:
apply mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt hV hW hs
    ((hf.mono hsu).of_le (le_minSmoothness.trans hn)) hx₀ hst

Premises used: ContMDiffWithinAt.mono, le_minSmoothness, ContMDiffWithinAt.of_le, VectorField.mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt, LE.le.trans
-- 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
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₀)
⊢ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s =ᶠ[𝓝 ((↑(extChartAt I x₀) : M → E) x₀)]
    (↑(extChartAt I x₀).symm : E → M) ⁻¹' s

Tactic:
rfl
-- 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
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₀)
⊢ (↑(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
-- 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
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)
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₀)
⊢ 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₀)

Tactic:
apply IsSymmSndFDerivWithinAt.congr_set _ this

Premises used: IsSymmSndFDerivWithinAt.congr_set
-- 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
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
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₀)
⊢ 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:
apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl

Premises used: le_rfl, ContDiffWithinAt.isSymmSndFDerivWithinAt
-- 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
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₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u)
⊢ UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' u ∩ (extChartAt I x₀).target)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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
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₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u)

Tactic:
UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀

Premises used: UniqueMDiffOn.uniqueDiffOn_target_inter
-- 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
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₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' u)

Tactic:
exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀

Premises used: UniqueMDiffOn.uniqueDiffOn_target_inter