awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x

Tactic:
exact hU.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

Tactic:
hV.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

Tactic:
exact hV.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
hW.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
exact hW.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffAt 𝕜 n U x
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
simp :
  ∀ (hU : ContDiffWithinAt 𝕜 n U univ x) (hV : ContDiffWithinAt 𝕜 n V univ x) (hW : ContDiffWithinAt 𝕜 n W univ x),
    lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W univ) univ x =
      lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V univ) W univ x +
        lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W univ) univ x
⊢ lieBracket 𝕜 U (lieBracket 𝕜 V W) x = lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x

Tactic:
simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊢

Premises used: contDiffWithinAt_univ, VectorField.lieBracketWithin_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffWithinAt 𝕜 n U univ x
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffWithinAt 𝕜 n U univ x
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V univ) W univ x +
      lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W univ) univ x

Tactic:
exact leibniz_identity_lieBracketWithin hn uniqueDiffOn_univ (by simp) (mem_univ _) hU hV hW

Premises used: uniqueDiffOn_univ, Set.mem_univ, VectorField.leibniz_identity_lieBracketWithin
-- 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
f : E → F
V : F → F
s : Set E
⊢ pullbackWithin 𝕜 f V s = fun (x : E) ↦ (ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (V (f x))

Tactic:
rfl

Premises used: VectorField.pullbackWithin, rfl
-- 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
f : E → F
M : E ≃L[𝕜] F
x : E
hf : (↑M : E →L[𝕜] F) = fderiv 𝕜 f x
V : F → F
⊢ pullback 𝕜 f V x = (M.symm : (a : F) → E) (V (f x))

Tactic:
simp [pullback, ← hf]

Premises used: VectorField.pullback
-- 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
f : E → F
x : E
h : ¬ContinuousLinearMap.IsInvertible (fderiv 𝕜 f x)
V : F → F
⊢ pullback 𝕜 f V x = 0

Tactic:
simp [pullback, h]

Premises used: VectorField.pullback
-- 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
f : E → F
x : E
h : ¬ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
V : F → F
⊢ pullbackWithin 𝕜 f V s x = 0

Tactic:
simp [pullbackWithin, h]

Premises used: VectorField.pullbackWithin
-- 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
f : E → F
M : E ≃L[𝕜] F
x : E
hf : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
V : F → F
⊢ pullbackWithin 𝕜 f V s x = (M.symm : (a : F) → E) (V (f x))

Tactic:
simp [pullbackWithin, ← hf]

Premises used: VectorField.pullbackWithin
-- 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
f : E → F
V : F → F
h : ∀ (x : E), pullbackWithin 𝕜 f V univ x = pullback 𝕜 f V x
⊢ pullbackWithin 𝕜 f V univ = pullback 𝕜 f V

Tactic:
ext x
-- 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
f : E → F
V : F → F
x : E
⊢ pullbackWithin 𝕜 f V univ x = pullback 𝕜 f V x

Tactic:
simp [pullbackWithin, pullback]

Premises used: VectorField.pullbackWithin, VectorField.pullback
-- 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
f : E → F
V : F → F
x : E
h'f : ContinuousLinearMap.IsInvertible (fderiv 𝕜 f x)
rcases :
  ∀ (M : E ≃L[𝕜] F) (hM : (↑M : E →L[𝕜] F) = fderiv 𝕜 f x), (fderiv 𝕜 f x : (a : E) → F) (pullback 𝕜 f V x) = V (f x)
⊢ (fderiv 𝕜 f x : (a : E) → F) (pullback 𝕜 f V x) = V (f x)

Tactic:
rcases h'f with ⟨M, hM⟩
-- 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
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderiv 𝕜 f x
⊢ (fderiv 𝕜 f x : (a : E) → F) (pullback 𝕜 f V x) = V (f x)

Tactic:
simp [pullback_eq_of_fderiv_eq hM, ← hM]

Premises used: VectorField.pullback_eq_of_fderiv_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
f : E → F
V : F → F
x : E
h'f : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
rcases :
  ∀ (M : E ≃L[𝕜] F) (hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x),
    (fderivWithin 𝕜 f s x : (a : E) → F) (pullbackWithin 𝕜 f V s x) = V (f x)
⊢ (fderivWithin 𝕜 f s x : (a : E) → F) (pullbackWithin 𝕜 f V s x) = V (f x)

Tactic:
rcases h'f with ⟨M, hM⟩
-- 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
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x : (a : E) → F) (pullbackWithin 𝕜 f V s x) = V (f x)

Tactic:
simp [pullbackWithin_eq_of_fderivWithin_eq hM, ← hM]

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
inst_5 : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
rcases :
  ∀ (M : E ≃L[𝕜] F) (hM : (↑M : E →L[𝕜] F) = fderivWithin 𝕜 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)
⊢ ∃ (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:
rcases hf with ⟨M, hM⟩
-- 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}
rw : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑M : E →L[𝕜] F)
⊢ Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)

Tactic:
rw [← hM]
-- 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}
⊢ range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑M : E →L[𝕜] F)

Tactic:
M.nhds

Premises used: Set.Mem, ContinuousLinearEquiv.nhds
-- 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}
⊢ range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑M : E →L[𝕜] F)

Tactic:
exact M.nhds

Premises used: ContinuousLinearEquiv.nhds
-- 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}
⊢ Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)

Tactic:
have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) := by
      rw [← hM]
      exact M.nhds
-- 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}
I :
  Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)
⊢ ContinuousWithinAt (Y := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x

Tactic:
have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
      (h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
-- 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}
I :
  Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)
this : ContinuousWithinAt (Y := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
⊢ U ∈ 𝓝[s] x

Tactic:
this I

Premises used: Set.Mem, setOf, Set.preimage, Set.range
-- 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}
I :
  Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)
this : ContinuousWithinAt (Y := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
⊢ U ∈ 𝓝[s] x

Tactic:
exact this I
-- 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}
⊢ U ∈ 𝓝[s] x

Tactic:
have hU : U ∈ 𝓝[s] x := by
    have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) := by
      rw [← hM]
      exact M.nhds
    have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
      (h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
    exact this I
-- 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
h : ∀ (y : E) (hy : y ∈ U), (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
⊢ (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y

Tactic:
filter_upwards [hU] with y 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
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
y : E
hy : y ∈ U
⊢ (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y

Tactic:
simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy

Premises used: Exists.choose_spec, reduceDIte
-- 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
⊢ (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y

Tactic:
have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y := by
    filter_upwards [hU] with y hy
    simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec 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
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
⊢ (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x

Tactic:
apply mem_of_mem_nhdsWithin hx eN

Premises used: mem_of_mem_nhdsWithin
-- 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
⊢ (↑(N x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x

Tactic:
have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN
-- 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) ↦ fderivWithin 𝕜 f s y) s x

Tactic:
have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x :=
      h'f.fderivWithin_right (m := 1) hs le_rfl hx