awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y_1 : ℕ → E
hy_1 : ∀ (n : ℕ), y_1 n ∈ interior s
y_lim : Tendsto y_1 atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y_1 k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y_1 k)
this : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s y)
    (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u) y)
have h : s =ᶠ[𝓝 y] s ∩ u
Tactic: apply fderivWithin_fderivWithin_eq_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y_1 : ℕ → E
hy_1 : ∀ (n : ℕ), y_1 n ∈ interior s
y_lim : Tendsto y_1 atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y_1 k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y_1 k)
this : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
⊢ s =ᶠ[𝓝 y] s ∩ u
have h : ∀ (z : E) (hz : z ∈ u), s z = (s ∩ u) z
Tactic: filter_upwards [u_open.mem_nhds hy.2] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y_1 : ℕ → E
hy_1 : ∀ (n : ℕ), y_1 n ∈ interior s
y_lim : Tendsto y_1 atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y_1 k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y_1 k)
this : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
z : E
hz : z ∈ u
⊢ s z = (s ∩ u) z
have h : (z ∈ s) = (z ∈ s ∩ u)
Tactic: change (z ∈ s) = (z ∈ s ∩ u)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
Tactic: have A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u) := by
    have : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u) :=
      ((hu.fderivWithin h'u (m := 1) (le_minSmoothness.trans hm)).fderivWithin h'u
      (m := 0) le_rfl).continuousOn
    apply this.congr
    intro y hy
    apply fderivWithin_fderivWithin_eq_of_eventuallyEq
    filter_upwards [u_open.mem_nhds hy.2] with z hz
    change (z ∈ s) = (z ∈ s ∩ u)
    simp_all
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
⊢ Tendsto y atTop (𝓝[s ∩ u] x)
have apply : ∀ᶠ (n : ℕ) in atTop, y n ∈ s ∩ u
Tactic: apply tendsto_nhdsWithin_iff.2 ⟨y_lim, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
⊢ ∀ᶠ (n : ℕ) in atTop, y n ∈ s ∩ u
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (k : ℕ) ↦ y k ∈ u) x} x →
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ y n ∈ s ∩ u) x} x}
    a
Tactic: filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (k : ℕ) ↦ y k ∈ u) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ y n ∈ s ∩ u) x} x}
      a
⊢ ∀ᶠ (n : ℕ) in atTop, y n ∈ s ∩ u
have h₁ : ∀ (a : ℕ), y a ∈ u → y a ∈ s ∩ u
Tactic: filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
⊢ Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
have this : Tendsto y atTop (𝓝[s ∩ u] x)
Tactic: have : Tendsto y atTop (𝓝[s ∩ u] x) := by
      apply tendsto_nhdsWithin_iff.2 ⟨y_lim, ?_⟩
      filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have B : Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
  (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
Tactic: have B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
      (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x)) := by
    have : Tendsto y atTop (𝓝[s ∩ u] x) := by
      apply tendsto_nhdsWithin_iff.2 ⟨y_lim, ?_⟩
      filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
    exact (A x ⟨h'x, xu⟩ ).tendsto.comp this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
v w : E
⊢ Tendsto.{0, u_3} (β := F)
    (fun (k : ℕ) ↦
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
    atTop
    (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
have this : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (A : E →L[𝕜] E →L[𝕜] F) ↦
  (((A : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w
Tactic: have : Continuous (fun (A : E →L[𝕜] E →L[𝕜] F) ↦ A v w) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have C : ∀ (v w : E),
  Tendsto.{0, u_3} (β := F)
    (fun (k : ℕ) ↦
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
    atTop
    (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
Tactic: have C (v w : E) : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) v w) atTop
      (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w)) := by
    have : Continuous (fun (A : E →L[𝕜] E →L[𝕜] F) ↦ A v w) := by fun_prop
    exact (this.tendsto _).comp B
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto.{0, u_3} (β := F)
      (fun (k : ℕ) ↦
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
      atTop
      (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
v w : E
⊢ Tendsto.{0, u_3} (β := F)
    (fun (k : ℕ) ↦
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F))
    atTop
    (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
have apply : EventuallyEq.{0, u_3} (β := F) atTop
  (fun (k : ℕ) ↦ (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w)
  fun (k : ℕ) ↦ (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v
Tactic: apply (C v w).congr'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto.{0, u_3} (β := F)
      (fun (k : ℕ) ↦
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
      atTop
      (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
v w : E
⊢ EventuallyEq.{0, u_3} (β := F) atTop
    (fun (k : ℕ) ↦
      (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w)
    fun (k : ℕ) ↦ (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (k : ℕ) ↦ IsSymmSndFDerivWithinAt 𝕜 f s (y k)) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                Eq.{u_3 + 1} (α := F)
                  ((fun (k : ℕ) ↦
                      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) :
                            (a : E) → F)
                          w :
                        F))
                    x)
                  ((fun (k : ℕ) ↦
                      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) :
                            (a : E) → F)
                          v :
                        F))
                    x))
              x}
          x}
    a
Tactic: filter_upwards [I] with k hk using hk v w
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto.{0, u_3} (β := F)
      (fun (k : ℕ) ↦
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
      atTop
      (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
v w : E
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (k : ℕ) ↦ IsSymmSndFDerivWithinAt 𝕜 f s (y k)) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_3 + 1} (α := F)
                    ((fun (k : ℕ) ↦
                        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) :
                              (a : E) → F)
                            w :
                          F))
                      x)
                    ((fun (k : ℕ) ↦
                        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) :
                              (a : E) → F)
                            v :
                          F))
                      x))
                x}
            x}
      a
⊢ EventuallyEq.{0, u_3} (β := F) atTop
    (fun (k : ℕ) ↦
      (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w)
    fun (k : ℕ) ↦ (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v
have h₁ : ∀ (a : ℕ),
  IsSymmSndFDerivWithinAt 𝕜 f s (y a) →
    Eq.{u_3 + 1} (α := F)
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y a) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y a) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)
Tactic: filter_upwards [I] with k hk using hk v w