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
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₀
⊢ ContDiffWithinAt 𝕜 ∞ (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₀
⊢ ContDiffWithinAt 𝕜 ∞ (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
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₀
m : ℕ
hg : ContDiffWithinAt 𝕜 (↑m) g s x₀
hmn : ↑m + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ↑m → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (↑m) (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₀
m : ℕ
hg : ContDiffWithinAt 𝕜 (↑m) g s x₀
hmn : ↑m + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ↑m → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (↑m) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
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 ≠ ∞
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
i : ℕ
h : n = ω
⊢ AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x 0) (v ∩ u)

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 : ℕ∞ω
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
i : ℕ
h : n = ω
⊢ AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x 0) (v ∩ u)
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 ≠ ∞
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
i✝ : ℕ
h : n = ω
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x (i + 1)) (v ∩ u)

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 : ℕ∞ω
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
i✝ : ℕ
h : n = ω
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x (i + 1)) (v ∩ u)
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
hn : n ≠ ω
hm : ω ≤ n
h' : ω = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 ω f (insert x s ∩ u)

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
m n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
hm : ω ≤ n
h' : ω = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 ω f (insert x s ∩ u)
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
hn : n ≠ ω
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 ∞ f (insert x s ∩ u)

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
m n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 ∞ f (insert x s ∩ u)
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
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)

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
m✝ n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
H : ContDiffOn 𝕜 (ω + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ω → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 ω (fderivWithin 𝕜 f s) 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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
H : ContDiffOn 𝕜 (ω + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ω → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 ω (fderivWithin 𝕜 f s) s x
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
H : ContDiffOn 𝕜 (∞ + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ∞ → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 ∞ (fderivWithin 𝕜 f s) 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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
H : ContDiffOn 𝕜 (∞ + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ∞ → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 ∞ (fderivWithin 𝕜 f s) s x
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
n✝ : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
n : ℕ
H : ContDiffOn 𝕜 (↑n + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ↑n → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 (↑n) (fderivWithin 𝕜 f s) 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
n✝ : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
n : ℕ
H : ContDiffOn 𝕜 (↑n + 1) f s
A : ∀ (m : ℕ), ↑m ≤ ↑n → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 (↑n) (fderivWithin 𝕜 f s) s x
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
f : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
hn : n ≠ 0
⊢ DifferentiableAt 𝕜 f x

Tactic:
by
  simpa [hn, differentiableWithinAt_univ] using h.differentiableWithinAt

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
f : E → F
n : ℕ∞ω
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f

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
f : E → F
n : ℕ∞ω
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f
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
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ContDiff 𝕜 (↑n) f

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
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ContDiff 𝕜 (↑n) f
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, none⟩) =
    ⟨c, none⟩

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, none⟩) =
    ⟨c, none⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, some i⟩) =
    ⟨c, some i⟩

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, some i⟩) =
    ⟨c, some i⟩
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ x ^ n / ↑n !)

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedDivisionRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CharZero 𝕂
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ x ^ n / ↑n !) (exp x)

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedDivisionRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CharZero 𝕂
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x) (exp x)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ c.applyOrderedFinpartition p (update v j z) m =
    update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)) m

Tactic:
simp only [applyOrderedFinpartition, ne_eq, h, not_false_eq_true,
      update_of_ne]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ (p m) (update v j z ∘ c.emb m) = (p m) (v ∘ c.emb m)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun x ↦ ‖p₁ x c.length - p₂ x c.length‖ * ∏ i, ‖q₂ x (c.partSize i)‖) =O[l] f

Tactic:
· have H₁ : (fun a ↦ p₁ a c.length - p₂ a c.length) =O[l] f := hpf _ c.length_le
    have H₂ : ∀ i, (q₂ · (c.partSize i)) =O[l] (1 : α → ℝ) := fun i ↦
      (hq₂_bdd _ <| c.partSize_le i).isBigO_one ℝ
    simpa using H₁.norm_norm.mul <| .finsetProd fun i _ ↦ (H₂ i).norm_left

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
h : ∀ (i : ι), ContDiffWithinAt 𝕜 ω (fun x ↦ Φ x i) s x
⊢ ContDiffWithinAt 𝕜 ω Φ s x

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
h : ∀ (i : ι), ContDiffWithinAt 𝕜 ω (fun x ↦ Φ x i) s x
⊢ ContDiffWithinAt 𝕜 ω Φ s x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x ↦ Φ x i) s x
⊢ ContDiffWithinAt 𝕜 (↑n) Φ s x

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x ↦ Φ x i) s x
⊢ ContDiffWithinAt 𝕜 (↑n) Φ s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a : ℕ
ha : 0 < update c.partSize j (c.partSize j + 1) j
h'a : 0 < c.partSize j + 1
⊢ (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨0, ha⟩ = cons e (v ∘ c.emb j) ⟨0, h'a⟩

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a : ℕ
ha : 0 < update c.partSize j (c.partSize j + 1) j
h'a : 0 < c.partSize j + 1
⊢ (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨0, ha⟩ = cons e (v ∘ c.emb j) ⟨0, h'a⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a✝ a : ℕ
ha : a + 1 < update c.partSize j (c.partSize j + 1) j
h'a : a + 1 < c.partSize j + 1
⊢ (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a + 1, ha⟩ = cons e (v ∘ c.emb j) ⟨a + 1, h'a⟩

Tactic:
| =>

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a✝ a : ℕ
ha : a + 1 < update c.partSize j (c.partSize j + 1) j
h'a : a + 1 < c.partSize j + 1
⊢ (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a + 1, ha⟩ = cons e (v ∘ c.emb j) ⟨a + 1, h'a⟩
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: ⊢ AnalyticOnNhd ℂ NormedSpace.exp univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: ⊢ AnalyticOnNhd ℝ NormedSpace.exp univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Goal state after: