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
this : ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x

Tactic:
apply this.congr_of_eventuallyEq eN e'N

Premises used: ContDiffWithinAt.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
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
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x

Tactic:
have hN : ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x := by
    have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x :=
      h'f.fderivWithin_right (m := 1) hs le_rfl hx
    apply this.congr_of_eventuallyEq eN e'N
-- 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
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x

Tactic:
have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
      (contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
-- 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
this : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x

Tactic:
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 : 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
this : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
h : ∀ (y : E), (↑(N y).symm : F →L[𝕜] E) = (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) y
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x

Tactic:
convert! this with y
-- 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
this : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
y : E
⊢ (↑(N y).symm : F →L[𝕜] E) = (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) y

Tactic:
simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]

Premises used: ContinuousLinearMap.inverse_equiv, Function.comp_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
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
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x

Tactic:
have hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x := by
    have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
      (contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
    convert! this with y
    simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]
-- 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
⊢ ∃ (N : E → E ≃L[𝕜] F),
    ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x ∧
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : 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:
⟨N, hN, hN', eN, fun v ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine :
  ∀ (v : 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)
⊢ ∃ (N : E → E ≃L[𝕜] F),
    ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x ∧
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : 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:
refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
-- 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 y : E
h :
  ∀ (x : F),
    Eq (α := 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) :
            (a : F) → F)
          x :
        F)
      ((ContinuousLinearMap.id 𝕜 F : (a : F) → F) x : F)
⊢ 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)

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 : 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 y : E
x_1 : F
⊢ Eq (α := 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) :
          (a : F) → F)
        x_1 :
      F)
    ((ContinuousLinearMap.id 𝕜 F : (a : F) → F) x_1 : F)

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
⊢ ∀ (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)

Tactic:
have A' y : ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E)
      = ContinuousLinearMap.id 𝕜 F := 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)
⊢ 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)

Tactic:
simp [A', fderivWithin_const_apply]

Premises used: fderivWithin_const_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
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)
⊢ 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)

Tactic:
have : fderivWithin 𝕜 (fun y ↦ ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F)
      ((N y).symm : F →L[𝕜] E)) s x v = 0 := by
    simp [A', fderivWithin_const_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
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)
    ((HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F)) (β :=
            ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F))
            ((((ContinuousLinearMap.precompR E (ContinuousLinearMap.compL 𝕜 F E F) :
                        (a : E →L[𝕜] F) → (E →L[𝕜] F →L[𝕜] E) →L[𝕜] E →L[𝕜] F →L[𝕜] F)
                      (↑(N x) : E →L[𝕜] F) :
                    (E →L[𝕜] F →L[𝕜] E) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F)) :
                  (a : E →L[𝕜] F →L[𝕜] E) → E →L[𝕜] F →L[𝕜] F)
                (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F))
            ((((ContinuousLinearMap.precompL E (ContinuousLinearMap.compL 𝕜 F E F) :
                        (a : E →L[𝕜] E →L[𝕜] F) → (F →L[𝕜] E) →L[𝕜] E →L[𝕜] F →L[𝕜] F)
                      (fderivWithin 𝕜 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x) :
                    (F →L[𝕜] E) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F)) :
                  (a : F →L[𝕜] E) → E →L[𝕜] F →L[𝕜] F)
                (↑(N x).symm : F →L[𝕜] E) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E (F →L[𝕜] F)) :
          (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:
simpa [eq_neg_iff_add_eq_zero] using this

Premises used: eq_neg_iff_add_eq_zero