awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
h₁ :
  (𝓝[s] x).EventuallyEq (β := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) fun (y : E) ↦
    ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
hx₁ :
  Eq.{u_2 + 1} (α := E) ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x)) : E)
    (((↑(M x).symm : F →L[𝕜] E) : (a : F) → E) (V (f x)) : E)
⊢ DifferentiableWithinAt 𝕜 (F := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x

Tactic:
apply this.congr_of_eventuallyEq

Premises used: DifferentiableWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
y : E
hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
⊢ Eq.{u_2 + 1} (α := E) ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s y) : (a : F) → E) (V (f y)) : E)
    (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y)) : E)

Tactic:
simp [← hy]
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              (fun (x : E) ↦
                  Eq.{u_2 + 1} (α := E)
                    ((fun (x : E) ↦ ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x)) : E))
                      x)
                    ((fun (y : E) ↦ (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y)) : E)) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (y : E) (hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y),
    Eq.{u_2 + 1} (α := E) ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s y) : (a : F) → E) (V (f y)) : E)
      (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y)) : E)
⊢ (𝓝[s] x).EventuallyEq (β := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) fun (y : E) ↦
    ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))

Tactic:
filter_upwards [hM] with y hy using by simp [← hy]
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
⊢ (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x

Tactic:
apply mem_of_mem_nhdsWithin hx hM

Premises used: mem_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
⊢ (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x

Tactic:
have hMx : M x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx hM
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
⊢ Eq.{u_2 + 1} (α := E) ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x)) : E)
    (((↑(M x).symm : F →L[𝕜] E) : (a : F) → E) (V (f x)) : E)

Tactic:
simp [← hMx]
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : ContinuousLinearMap.IsInvertible (fderiv 𝕜 f x)
simp :
  ∀ (hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f univ x)) (h'f : ContDiffWithinAt 𝕜 2 f univ x),
    ∃ (N : E → E ≃L[𝕜] F),
      ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) univ x ∧
        ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x ∧
          (∀ᶠ (y : E) in 𝓝[univ] x, (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f univ y) ∧
            ∀ (v : E),
              (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x : (a : E) → F →L[𝕜] E) v =
                -(↑(N x).symm : F →L[𝕜] E) ∘SL
                    ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                      ((fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x : (a : E) → E →L[𝕜] F) v)
                      (↑(N x).symm : F →L[𝕜] E)
⊢ ∃ (N : E → E ≃L[𝕜] F),
    ContDiffAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) x ∧
      ContDiffAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) x ∧
        (∀ᶠ (y : E) in 𝓝 x, (↑(N y) : E →L[𝕜] F) = fderiv 𝕜 f y) ∧
          ∀ (v : E),
            (fderiv 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) x : (a : E) → F →L[𝕜] E) v =
              -(↑(N x).symm : F →L[𝕜] E) ∘SL
                  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((fderiv 𝕜 (fderiv 𝕜 f) x : (a : E) → E →L[𝕜] F) v)
                    (↑(N x).symm : F →L[𝕜] E)

Tactic:
simp only [← fderivWithin_univ, ← contDiffWithinAt_univ, ← nhdsWithin_univ] at hf h'f ⊢

Premises used: contDiffWithinAt_univ, nhdsWithin_univ, fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
x : E
hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f univ x)
h'f : ContDiffWithinAt 𝕜 2 f univ x
⊢ ∃ (N : E → E ≃L[𝕜] F),
    ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) univ x ∧
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x ∧
        (∀ᶠ (y : E) in 𝓝[univ] x, (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f univ y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x : (a : E) → F →L[𝕜] E) v =
              -(↑(N x).symm : F →L[𝕜] E) ∘SL
                  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                    ((fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)

Tactic:
exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, exists_continuousLinearEquiv_fderivWithin_symm_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
x : E
hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f univ x)
h'f : ContDiffWithinAt 𝕜 2 f univ x
⊢ ∃ (N : E → E ≃L[𝕜] F),
    ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) univ x ∧
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x ∧
        (∀ᶠ (y : E) in 𝓝[univ] x, (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f univ y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) univ x : (a : E) → F →L[𝕜] E) v =
              -(↑(N x).symm : F →L[𝕜] E) ∘SL
                  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                    ((fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)

Tactic:
exact exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, exists_continuousLinearEquiv_fderivWithin_symm_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
pos :
  ∀ (h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)),
    pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
      lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
neg :
  ∀ (h : ¬ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)),
    pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
      lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
by_cases h : (fderivWithin 𝕜 f s x).IsInvertible

Premises used: ContinuousLinearMap.IsInvertible, fderivWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ¬ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
simp [pullbackWithin_eq_of_not_isInvertible h, lieBracketWithin_eq]

Premises used: VectorField.pullbackWithin_eq_of_not_isInvertible, VectorField.lieBracketWithin_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
pos :
  ∀ (M : E → E ≃L[𝕜] F)
    (M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x)
    (hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y)
    (M_diff :
      ∀ (v : E),
        (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
          -(↑(M x).symm : F →L[𝕜] E) ∘SL
              ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)),
    pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
      lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
rcases exists_continuousLinearEquiv_fderivWithin_symm_eq h'f h hu hx
    with ⟨M, -, M_symm_smooth, hM, M_diff⟩

Premises used: exists_continuousLinearEquiv_fderivWithin_symm_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
⊢ (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x

Tactic:
have hMx : M x = fderivWithin 𝕜 f s x := (mem_of_mem_nhdsWithin hx hM :)
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
apply : pullbackWithin 𝕜 f V s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x)

Tactic:
apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx

Premises used: Filter.EventuallyEq.fderivWithin_eq_of_mem
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
y : E
hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
⊢ pullbackWithin 𝕜 f V s y = ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))

Tactic:
pullbackWithin_eq_of_fderivWithin_eq hy _

Premises used: VectorField.pullbackWithin_eq_of_fderivWithin_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              (fun (x : E) ↦
                  pullbackWithin 𝕜 f V s x =
                    (fun (y : E) ↦ (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y)) : E)) x)
                x}
            x}
      a
h₂ h₃ :
  ∀ (y : E) (hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y),
    pullbackWithin 𝕜 f V s y = ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
⊢ pullbackWithin 𝕜 f V s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))

Tactic:
filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x)

Tactic:
have AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x =
      fderivWithin 𝕜 (fun y ↦ ((M y).symm : F →L[𝕜] E) (V (f y))) s x := by
    apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx
    filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _