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
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 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
have h : ∀ (y : E), (↑(N y).symm : F →L[𝕜] E) = (ContinuousLinearMap.inverse ∘ fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) y
Tactic: convert! this with y
-- 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
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
⊢ ∃ (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)
have hN' : 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]
-- 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
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)
have 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)
Tactic: refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
-- 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
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
⊢ 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)
have 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)
Tactic: ext
-- 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
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
⊢ (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)
have 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)
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
-- 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
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)
⊢ (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)
have 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)
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]
-- 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
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)
⊢ (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)
have 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)
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
-- 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
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
⊢ M = (↑(N x).symm : F →L[𝕜] E) ∘SL (↑(N x) : E →L[𝕜] F) ∘SL M
have 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)
Tactic: ext
-- 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
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)
⊢ (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)
have B : ∀ (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
-- 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
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
⊢ (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)
have 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)
Tactic: rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]
-- 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
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x
have 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
Tactic: rcases exists_continuousLinearEquiv_fderivWithin_symm_eq hf hf' hs hx
    with ⟨M, -, M_symm_smooth, 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
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 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x
have simp : DifferentiableWithinAt 𝕜 (F := E)
  (fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))) s x
Tactic: simp only [pullbackWithin_eq]