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
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
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)
apply : pullbackWithin 𝕜 f W s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (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
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)
y : E
hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
⊢ pullbackWithin 𝕜 f W s y = ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (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
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)
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 W s x =
                    (fun (y : E) ↦ (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y)) : E)) x)
                x}
            x}
      a
h₂ h₃ :
  ∀ (y : E) (hy : (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y),
    pullbackWithin 𝕜 f W s y = ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))
⊢ pullbackWithin 𝕜 f W s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
have Af : DifferentiableWithinAt 𝕜 f s x := h'f.differentiableWithinAt two_ne_zero
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
pos :
  HSub.hSub (α := E) (β := E) (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 W t (f x) : (a : F) → F) (V (f x)) : F) : E)
      (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 V t (f x) : (a : F) → F) (W (f x)) : F) : E) =
    HSub.hSub (α := E) (β := E)
      ((fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x : (a : E) → E)
          (((M x).symm : (a : F) → E) (V (f x)) : E) :
        E)
      ((fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x : (a : E) → E)
          (((M x).symm : (a : F) → E) (W (f x)) : E) :
        E)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
simp only [lieBracketWithin_eq, pullbackWithin_eq_of_fderivWithin_eq hMx, map_sub, AV, AW]

Premises used: map_sub, VectorField.pullbackWithin_eq_of_fderivWithin_eq, 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)
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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ HSub.hSub (α := E) (β := E) (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 W t (f x) : (a : F) → F) (V (f x)) : F) : E)
      (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 V t (f x) : (a : F) → F) (W (f x)) : F) : E) =
    HSub.hSub (α := E) (β := E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
              ((↑(M x).symm : F →L[𝕜] E) ∘SL fderivWithin 𝕜 (fun (y : E) ↦ W (f y)) s x)
              ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x) :
                    (a : F) → E →L[𝕜] E)
                  (W (f x)) :
                E →L[𝕜] E) :
            (a : E) → E)
          (((M x).symm : (a : F) → E) (V (f x)) : E) :
        E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
              ((↑(M x).symm : F →L[𝕜] E) ∘SL fderivWithin 𝕜 (fun (y : E) ↦ V (f y)) s x)
              ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x) :
                    (a : F) → E →L[𝕜] E)
                  (V (f x)) :
                E →L[𝕜] E) :
            (a : E) → E)
          (((M x).symm : (a : F) → E) (W (f x)) : E) :
        E)

Tactic:
simp [fderivWithin_comp' x hW Af hst (hu x hx), ← hMx,
      fderivWithin_comp' x hV Af hst (hu x hx), M_diff, hf.eq]

Premises used: fderivWithin_comp', IsSymmSndFDerivWithinAt.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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
hu x hx
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
exact hu x hx
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (F := F →L[𝕜] E) (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x

Tactic:
M_symm_smooth.differentiableWithinAt one_ne_zero

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (F := F →L[𝕜] E) (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x

Tactic:
exact M_symm_smooth.differentiableWithinAt one_ne_zero

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x

Tactic:
hV.comp x Af hst

Premises used: DifferentiableWithinAt.comp
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x

Tactic:
exact hV.comp x Af hst

Premises used: DifferentiableWithinAt.comp
-- 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
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)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ W (f y)) s x

Tactic:
hW.comp x Af hst

Premises used: DifferentiableWithinAt.comp