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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
⊢ (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)

Tactic:
have I : (N x : E →L[𝕜] F) ∘L (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v) =
      - (fderivWithin 𝕜 (fun y ↦ (N y : E →L[𝕜] F)) s x v) ∘L ((N x).symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.fderivWithin_of_bilinear _ (hN.differentiableWithinAt one_ne_zero)
      (hN'.differentiableWithinAt one_ne_zero) (hs x hx)] at this
    simpa [eq_neg_iff_add_eq_zero] using this
-- 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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M_1 : E ≃L[𝕜] F
hM : (↑M_1 : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M_1
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
I :
  (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
M : F →L[𝕜] E
h :
  ∀ (x_1 : F),
    Eq.{u_2 + 1} (α := E) ((M : (a : F) → E) x_1 : E)
      (((↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M : (a : F) → E) x_1 : E)
⊢ M = (↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M

Tactic:
ext
-- 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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M_1 : E ≃L[𝕜] F
hM : (↑M_1 : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M_1
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
I :
  (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
M : F →L[𝕜] E
x_1 : F
⊢ Eq.{u_2 + 1} (α := E) ((M : (a : F) → E) x_1 : E)
    (((↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M : (a : F) → E) x_1 : E)

Tactic:
simp
-- 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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
I :
  (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
⊢ ∀ (M : F →L[𝕜] E), M = (↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M

Tactic:
have B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by
    ext; simp
-- 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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
I :
  (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
B : ∀ (M : F →L[𝕜] E), M = (↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M
rw :
  (↑(N x).symm : F →L[𝕜] E) ∘SL
      (-ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v)
          (↑(N x).symm : F →L[𝕜] E)) =
    -(↑(N x).symm : F →L[𝕜] E) ∘SL
        ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
⊢ (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
    -(↑(N x).symm : F →L[𝕜] E) ∘SL
        ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)

Tactic:
rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]

Premises used: ContinuousLinearEquiv.symm, fderivWithin, DFunLike.coe, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
U : Set E := {y : E | ∃ (N : E ≃L[𝕜] F), (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F :=
  fun (x : E) ↦
    if h : x ∈ U then Exists.choose (p := fun (N : E ≃L[𝕜] F) ↦ (↑N : E →L[𝕜] F) = fderivWithin 𝕜 f s x) h else M
eN : (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
e'N : (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
hN' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
v : E
A' :
  ∀ (y : E),
    Eq.{u_3 + 1} (α := F →L[𝕜] F)
      ((((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) (↑(N y) : E →L[𝕜] F) :
              (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
            (a : F →L[𝕜] E) → F →L[𝕜] F)
          (↑(N y).symm : F →L[𝕜] E) :
        F →L[𝕜] F)
      (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
this :
  Eq.{u_3 + 1} (α := F →L[𝕜] F)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (((ContinuousLinearMap.compL 𝕜 F E F : (a : E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F)
                      (↑(N y) : E →L[𝕜] F) :
                    (F →L[𝕜] E) →L[𝕜] F →L[𝕜] F) :
                  (a : F →L[𝕜] E) → F →L[𝕜] F)
                (↑(N y).symm : F →L[𝕜] E))
            s x :
          (a : E) → F →L[𝕜] F)
        v :
      F →L[𝕜] F)
    (0 : F →L[𝕜] F)
I :
  (↑(N x) : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜)
      ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v) =
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)
B : ∀ (M : F →L[𝕜] E), M = (↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M
⊢ (↑(N x).symm : F →L[𝕜] E) ∘SL
      (-ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x : (a : E) → E →L[𝕜] F) v)
          (↑(N x).symm : F →L[𝕜] E)) =
    -(↑(N x).symm : F →L[𝕜] E) ∘SL
        ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(N x).symm : F →L[𝕜] E)

Tactic:
simp only [ContinuousLinearMap.comp_neg, eN.fderivWithin_eq e'N]

Premises used: ContinuousLinearMap.comp_neg, Filter.EventuallyEq.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
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
rcases :
  ∀ (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 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

Tactic:
rcases exists_continuousLinearEquiv_fderivWithin_symm_eq hf hf' hs hx
    with ⟨M, -, M_symm_smooth, hM, -⟩

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
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
simp :
  DifferentiableWithinAt 𝕜 (F := E)
    (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

Tactic:
simp only [pullbackWithin_eq]

Premises used: VectorField.pullbackWithin_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
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
hu : DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x
⊢ DifferentiableWithinAt 𝕜 (F := E) (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x

Tactic:
apply DifferentiableWithinAt.clm_apply

Premises used: DifferentiableWithinAt.clm_apply
-- 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
⊢ 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
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 := 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
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.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x

Tactic:
hV.comp _ (hf.differentiableWithinAt two_ne_zero) hst

Premises used: DifferentiableWithinAt.comp, two_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
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.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ V (f y)) s x

Tactic:
exact hV.comp _ (hf.differentiableWithinAt two_ne_zero) hst

Premises used: DifferentiableWithinAt.comp, two_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
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

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