awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
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
⊢ 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:
exact (this.tendsto _).comp B

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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)

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
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
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
⊢ 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)

Tactic:
apply (C v w).congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
k : ℕ
hk : IsSymmSndFDerivWithinAt 𝕜 f s (y k)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
hk v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
h₁ h₂ :
  ∀ (k : ℕ) (hk : IsSymmSndFDerivWithinAt 𝕜 f s (y k)),
    Eq.{u_3 + 1} (α := F)
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)
⊢ 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:
filter_upwards [I] with k hk using hk v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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)

Tactic:
have C' (v w : E) : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) w v) atTop
      (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w)) := by
    apply (C v w).congr'
    filter_upwards [I] with k hk using hk v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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)
C' :
  ∀ (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)
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
tendsto_nhds_unique (C v w) (C' w v)

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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)
C' :
  ∀ (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)
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
exact tendsto_nhds_unique (C v w) (C' w v)

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
have :
  ∀ (this : Fintype ι),
    DifferentiableWithinAt 𝕜 f t y ↔
      ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
⊢ DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
this : Fintype ι
rw :
  (∀ (i : ι),
      DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
⊢ DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableWithinAt_iff,
    differentiableWithinAt_pi]

Premises used: differentiableWithinAt_pi, ContinuousLinearEquiv.comp_differentiableWithinAt_iff, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
y : H
have :
  ∀ (this : Fintype ι),
    DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
y : H
this : Fintype ι
rw :
  (∀ (i : ι),
      DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableAt_iff, differentiableAt_pi]

Premises used: ContinuousLinearEquiv.comp_differentiableAt_iff, differentiableAt_pi, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
have :
  ∀ (this : Fintype ι),
    DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
rw :
  (∀ (i : ι),
      DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableOn_iff, differentiableOn_pi]

Premises used: differentiableOn_pi, ContinuousLinearEquiv.comp_differentiableOn_iff, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ (∀ (i : ι),
      DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i)
        (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
have :
  ∀ (this : Fintype ι),
    Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i

Tactic:
have := Fintype.ofFinite ι