awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
⊢ HSub.hSub (α := E)
      ((fderivWithin 𝕜
              (fun (x : E) ↦
                HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
                  ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E))
              s x :
            (a : E) → E)
          (U x) :
        E)
      (HSub.hSub (α := E) (β := E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E) : E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E) : E)) =
    HSub.hSub (β := E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E) : E))
        ((fderivWithin 𝕜
                (fun (x : E) ↦
                  HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E)
                    ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E))
                s x :
              (a : E) → E)
            (W x) :
          E) +
      HSub.hSub (α := E)
        ((fderivWithin 𝕜
                (fun (x : E) ↦
                  HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E)
                    ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E))
                s x :
              (a : E) → E)
            (V x) :
          E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E) : E))
have aux₁ : ∀ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x),
  DifferentiableWithinAt 𝕜 (F := E) (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (U x)) s x
Tactic: have aux₁ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
      DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x :=
    have := hV.fderivWithin_right_apply (hU.of_le one_le_two) hs le_rfl hx
    this.differentiableWithinAt one_ne_zero
-- 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
U_1 V_1 W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU_1 : ContDiffWithinAt 𝕜 2 U_1 s x
hV_1 : ContDiffWithinAt 𝕜 2 V_1 s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U_1 s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V_1 s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
aux₁ :
  ∀ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x),
    DifferentiableWithinAt 𝕜 (F := E) (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (U x)) s x
U V : E → E
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ (fderivWithin 𝕜 U s y : (a : E) → E) (V y)) s x =
    HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 U s x ∘SL fderivWithin 𝕜 V s x)
      ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x) : (a : E) → E →L[𝕜] E) (V x) : E →L[𝕜] E)
have refine : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E) (fderivWithin 𝕜 U s) s x
Tactic: refine fderivWithin_clm_apply (hs x hx) ?_ (hV.differentiableWithinAt two_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x
have h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
Tactic: apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx
    (hU.of_le (le_minSmoothness.trans hn)) (hV.of_le (le_minSmoothness.trans hn))
    (hW.of_le (le_minSmoothness.trans hn))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x
have h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
Tactic: apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx
    (hU.of_le (le_minSmoothness.trans hn)) (hV.of_le (le_minSmoothness.trans hn))
    (hW.of_le (le_minSmoothness.trans hn))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x
have h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
Tactic: apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx
    (hU.of_le (le_minSmoothness.trans hn)) (hV.of_le (le_minSmoothness.trans hn))
    (hW.of_le (le_minSmoothness.trans hn))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracket 𝕜 U (lieBracket 𝕜 V W) x = lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x
have 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
Tactic: simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊢
Cleared hypotheses: hU, hV, hW
-- 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
f : E → F
V : F → F
⊢ pullbackWithin 𝕜 f V univ = pullback 𝕜 f V
have h : ∀ (x : E), pullbackWithin 𝕜 f V univ x = pullback 𝕜 f V x
Tactic: ext x
-- 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
f : E → F
V : F → F
x : E
h'f : ContinuousLinearMap.IsInvertible (fderiv 𝕜 f x)
⊢ (fderiv 𝕜 f x : (a : E) → F) (pullback 𝕜 f V x) = V (f x)
have 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)
Tactic: rcases h'f with ⟨M, hM⟩
Cleared hypotheses: h'f
-- 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
s : Set E
f : E → F
V : F → F
x : E
h'f : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
⊢ (fderivWithin 𝕜 f s x : (a : E) → F) (pullbackWithin 𝕜 f V s x) = V (f x)
have 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)
Tactic: rcases h'f with ⟨M, hM⟩
Cleared hypotheses: h'f
-- 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
hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ∃ (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 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)
Tactic: rcases hf with ⟨M, hM⟩
Cleared hypotheses: hf
-- 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}
⊢ Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)
have rw : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑M : E →L[𝕜] F)
Tactic: rw [← hM]
-- 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}
⊢ U ∈ 𝓝[s] x
have I : 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
-- 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}
I :
  Membership.mem (γ := Filter (E →L[𝕜] F)) (𝓝 (fderivWithin 𝕜 f s x))
    (range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap)
⊢ U ∈ 𝓝[s] x
have this : 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
-- 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}
⊢ ∃ (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 hU : 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
-- 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
⊢ (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) fun (y : E) ↦ fderivWithin 𝕜 f s y
have h : ∀ (y : E) (hy : y ∈ U), (↑(N y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
Tactic: filter_upwards [hU] with y hy
-- 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
⊢ ∃ (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 eN : (𝓝[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
-- 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
⊢ ∃ (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 e'N : (↑(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
-- 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
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) 1 (fun (y : E) ↦ (↑(N y) : E →L[𝕜] F)) s x
have this : 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
-- 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
⊢ ∃ (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 := 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
-- 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
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(N y).symm : F →L[𝕜] E)) s x
have this : 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