mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ AnalyticOn 𝕜 f w

Tactic:
by

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

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
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set F
g : F → G
f : E → F
hg : ContDiffOn 𝕜 n g s
hf : ContDiff 𝕜 n f
hs : ∀ (x : E), f x ∈ s
⊢ ContDiff 𝕜 n (g ∘ f)

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
by

Goal state after:
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
f : E → F
g : F → G
n : ℕ∞ω
y : F
x : E
hg : ContDiffAt 𝕜 n g y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
by

Goal state after:
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
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
u : Set E
hu :
  ∀ ⦃x : Set E⦄,
    x ∈ 𝒫 (u ∩ s) →
      HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) x ∧
        HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' x)
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
⊢ s ∩ u ∈ 𝒫 (u ∩ s)

Tactic:
by

Goal state after:
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
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
⊢ ∃ u,
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
by

Goal state after:
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
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (g ∘ f) s x = (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i

Tactic:
by

Goal state after:
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
f : E → F
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i

Tactic:
by

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

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
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (fun y ↦ (f y, g y)) (fun y k ↦ (p y k).prod (q y k)) s

Tactic:
by

Goal state after:
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
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
hi : ↑(i + 1) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ ↑i < ↑(i + 1)

Tactic:
by

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

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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ (f x, g x)) s x

Tactic:
by

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
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (fun x ↦ p x 0) s
⊢ AnalyticOn 𝕜 f s

Tactic:
by

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
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
by

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
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ x ∈ insert x s

Tactic:
by

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
h : ContDiffWithinAt 𝕜 ω f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
by

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
inst✝ : CompleteSpace F
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
by

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 : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ (n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u)

Tactic:
by

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

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
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
⊢ iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x =
    (iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)

Tactic:
by

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

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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (fun x ↦ (f x, g x)) x = (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x)

Tactic:
by

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
m n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hmn : m ≤ n
⊢ ContDiffWithinAt 𝕜 m f s x

Tactic:
by

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
⊢ (∀ (m : ℕ), ↑m ≤ ⊤ → ContDiffWithinAt 𝕜 (↑m) f s x) ↔ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
by

Goal state after:
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
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
i : ℕ
hi : ↑i ≤ n
x : E
hx : x ∈ s
u : F
m : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u

Tactic:
by

Goal state after:
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
n : ℕ∞ω
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : ↑i ≤ n
x : E
u : F
m : Fin i → E
⊢ (iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u

Tactic:
by

Goal state after:
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)

Tactic:
by

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
⊢ ContinuousWithinAt f s x

Tactic:
by

Goal state after:
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
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₀
⊢ insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)

Tactic:
by

Goal state after:
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
⊢ ContDiff 𝕜 n f

Tactic:
by

Goal state after:
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)
⊢ ContDiffOn 𝕜 n f (⋃ i, s i)

Tactic:
by

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 f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
by

Goal state after:
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
⊢ ContDiff 𝕜 n f

Tactic:
by

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
t : Set E
hst : s ∈ 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
by

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
t : Set E
hst : s =ᶠ[𝓝 x] t
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
by

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 : UniqueDiffOn 𝕜 s
⊢ derivWithin f s = ⇑ContinuousLinearMap.toSpanSingletonCLE.symm ∘ fderivWithin 𝕜 f s

Tactic:
by

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 : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s

Tactic:
by

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
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 1 f s ↔ DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
by

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 : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
by

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 : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
by

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 : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
by

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
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s

Tactic:
by

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
hn : n ≠ 0
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
by

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
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s

Tactic:
by

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 : ℕ∞ω
hn : n ≠ ∞
⊢ n + 1 ≠ ∞

Tactic:
by

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 : ℕ∞ω
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 : HasFTaylorSeriesUpToOn (n + 1) f p u
H'p : n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
y : E
hy : y ∈ u
⊢ n + 1 ≠ 0

Tactic:
by

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
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (deriv f) s

Tactic:
by

Goal state after: