-- Mathlib/Geometry/Manifold/VectorField.lean
theorem mlieBracketWithin_of_mem_nhdsWithin
    (st : t ∈ 𝓝[s] x) (hs : UniqueMDiffWithinAt I s x)
    (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) t x)
    (hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) t x) :
    mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Proof state:
case h.e_6.h.st
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
apply Filter.inter_mem

Result:
case h.e_6.h.st.hs
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

case h.e_6.h.st.ht
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ range ↑I ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Proof state:
case h.e_6.h.st.ht
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ range ↑I ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
exact nhdsWithin_mono _ inter_subset_right self_mem_nhdsWithin

Result:
no goals

Proof state:
case h.e_6.h.hV
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact hV.differentiableWithinAt_mpullbackWithin_vectorField

Result:
no goals

Proof state:
case h.e_6.h.st.hs
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
apply nhdsWithin_mono _ inter_subset_left

Result:
case h.e_6.h.st.hs.a
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x

Proof state:
case h.e_6.h.st.hs.a
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) t x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) t x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x

Tactic:
exact (continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
  st (by simp)

Result:
no goals