mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.snd 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
]

Goal state after:
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.snd 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((iteratedFDerivWithin 𝕜 i c s x) (Fin.tail m) ∘SL 0 +
        (fderivWithin 𝕜 (fun y ↦ (iteratedFDerivWithin 𝕜 i c s y) (Fin.tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((iteratedFDerivWithin 𝕜 i c s x) (Fin.tail m) ∘SL 0 +
        (fderivWithin 𝕜 (fun y ↦ (iteratedFDerivWithin 𝕜 i c s y) (Fin.tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : ⋃ i, s i = univ
⊢ ContDiffOn 𝕜 n f (⋃ i, s i)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : ⋃ i, s i = univ
⊢ ContDiffOn 𝕜 n f (⋃ i, s i)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀) ≤ 𝓝[insert x₀ s ×ˢ t] (x₀, g x₀)
v : Set (E × F)
hv : 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀) ≤ 𝓝[v] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ 𝓝[(fun x ↦ (id x, g x)) '' s] (id x₀, g x₀) ≤ 𝓝[v] (id x₀, g x₀)

Tactic:
]

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀) ≤ 𝓝[insert x₀ s ×ˢ t] (x₀, g x₀)
v : Set (E × F)
hv : 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀) ≤ 𝓝[v] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ 𝓝[(fun x ↦ (id x, g x)) '' s] (id x₀, g x₀) ≤ 𝓝[v] (id x₀, g x₀)
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (0 = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (0 = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f s) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ 0
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑1) f p u
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
tu : insert x s ∩ t ⊆ u
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ 0
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑1) f p u
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
tu : insert x s ∩ t ⊆ u
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (deriv f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (deriv f) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (deriv f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (deriv f) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (deriv f) s

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (deriv f) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 0 (deriv f) ↔
    Differentiable 𝕜 f ∧ Continuous (deriv f)

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 0 (deriv f) ↔
    Differentiable 𝕜 f ∧ Continuous (deriv f)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mp.refine_2.refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) u
H'p : n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ HasFTaylorSeriesUpToOn n (fun y ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p y 1)) (fun y ↦ (p y).shift) u ∧
    (n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun y ↦ (p y).shift) x i) u)

Tactic:
]

Goal state after:
case mp.refine_2.refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) u
H'p : n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ HasFTaylorSeriesUpToOn n (fun y ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p y 1)) (fun y ↦ (p y).shift) u ∧
    (n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun y ↦ (p y).shift) x i) u)
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (deriv f)

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (deriv f)
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 0 + 1 ≤ n
⊢ Continuous (deriv f)

Tactic:
]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 0 + 1 ≤ n
⊢ Continuous (deriv f)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ p, HasFTaylorSeriesUpToOn (n + 1) f p u ∧ (n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u)

Tactic:
]

Goal state after:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ p, HasFTaylorSeriesUpToOn (n + 1) f p u ∧ (n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u)
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : ↑k ≤ m
⊢ n ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr.refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ (∀ x ∈ v ∩ u, ((p' x).unshift (f x) 0).curry0 = f x) ∧
    (∀ x ∈ v ∩ u, HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' x).unshift (f x) 1).curryLeft (v ∩ u) x) ∧
      HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1))
        (fun x ↦ ((p' x).unshift (f x)).shift) (v ∩ u)

Tactic:
]

Goal state after:
case mpr.refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ (∀ x ∈ v ∩ u, ((p' x).unshift (f x) 0).curry0 = f x) ∧
    (∀ x ∈ v ∩ u, HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' x).unshift (f x) 1).curryLeft (v ∩ u) x) ∧
      HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1))
        (fun x ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ∞ g s x₀
hmn : ∞ + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ∞ → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ∞ g s x₀
hmn : ∞ + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ∞ → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀