awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
have hc : DifferentiableWithinAt 𝕜 (F := F →L[𝕜] E) (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
Tactic: apply DifferentiableWithinAt.clm_apply
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
hc : DifferentiableWithinAt 𝕜 (F := F →L[𝕜] E) (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
⊢ DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
have hu : DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x
Tactic: apply DifferentiableWithinAt.clm_apply
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ DifferentiableWithinAt 𝕜 (F := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x
have this : DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x
Tactic: have : DifferentiableWithinAt 𝕜 (fun y ↦ ((M y).symm : F →L[𝕜] E) (V (f y))) s x := by
    apply DifferentiableWithinAt.clm_apply
    · exact M_symm_smooth.differentiableWithinAt one_ne_zero
    · exact hV.comp _ (hf.differentiableWithinAt two_ne_zero) hst
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ DifferentiableWithinAt 𝕜 (F := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x
have 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))
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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))
⊢ DifferentiableWithinAt 𝕜 (F := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x
have 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)
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ (𝓝[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))
have 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
Tactic: filter_upwards [hM] with y hy using by simp [← hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ (𝓝[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))
have h₁ : ∀ (a : E),
  (↑(M a) : E →L[𝕜] F) = fderivWithin 𝕜 f s a →
    Eq.{u_2 + 1} (α := E) ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s a) : (a : F) → E) (V (f a)) : E)
      (((↑(M a).symm : F →L[𝕜] E) : (a : F) → E) (V (f a)) : E)
Tactic: filter_upwards [hM] with y hy using by simp [← hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ 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)
have hMx : (↑(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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: simp only [← fderivWithin_univ, ← contDiffWithinAt_univ, ← nhdsWithin_univ] at hf h'f ⊢
Cleared hypotheses: h'f, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have 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
Tactic: by_cases h : (fderivWithin 𝕜 f s x).IsInvertible
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have 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
Tactic: by_cases h : (fderivWithin 𝕜 f s x).IsInvertible
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
have 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
Tactic: rcases exists_continuousLinearEquiv_fderivWithin_symm_eq h'f h hu hx
    with ⟨M, -, M_symm_smooth, hM, M_diff⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
Tactic: have hMx : M x = fderivWithin 𝕜 f s x := (mem_of_mem_nhdsWithin hx hM :)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
have apply : pullbackWithin 𝕜 f V s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
Tactic: apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f V s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
have 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
Tactic: filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f V s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))
have h₂ : ∀ (a : E),
  (↑(M a) : E →L[𝕜] F) = fderivWithin 𝕜 f s a →
    pullbackWithin 𝕜 f V s a = ((↑(M a).symm : F →L[𝕜] E) : (a : F) → E) (V (f a))
Tactic: filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have AV : 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 _