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

Goal state before:
pp: case mpr.refine_1
𝕜 : 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
⊢ v ∩ u ∈ 𝓝[insert x s] x

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
⊢ HasFTaylorSeriesUpToOn (n + 1) f (fun x ↦ (p' x).unshift (f x)) (v ∩ u)

pp: case mpr.refine_3
𝕜 : 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
⊢ n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x i) (v ∩ u)

Tactic:
·

Goal state after:
case mpr.refine_1
𝕜 : 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
⊢ v ∩ u ∈ 𝓝[insert x s] x
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
⊢ HasFTaylorSeriesUpToOn (n + 1) f (fun x ↦ (p' x).unshift (f x)) (v ∩ u)

pp: case mpr.refine_3
𝕜 : 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
⊢ n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x i) (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
⊢ HasFTaylorSeriesUpToOn (n + 1) f (fun x ↦ (p' x).unshift (f x)) (v ∩ u)
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case hf_emb
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Topology.IsEmbedding ⇑f'

pp: case ho
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ (fun x ↦
      match x with
      | (x, y) => g x - g y - (f'symm ∘SL h') (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)

Tactic:
·

Goal state after:
case hf_emb
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Topology.IsEmbedding ⇑f'
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case ho
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ (fun x ↦
      match x with
      | (x, y) => g x - g y - (f'symm ∘SL h') (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)

Tactic:
·

Goal state after:
case ho
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ (fun x ↦
      match x with
      | (x, y) => g x - g y - (f'symm ∘SL h') (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr.refine_2.refine_1
𝕜 : 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
y : E
hy : y ∈ v ∩ u
⊢ HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' y).unshift (f y) 1).curryLeft (v ∩ u) y

pp: case mpr.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 ≠ ∞
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
⊢ 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.refine_1
𝕜 : 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
y : E
hy : y ∈ v ∩ u
⊢ HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' y).unshift (f y) 1).curryLeft (v ∩ u) y
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Tendsto (Prod.map g g) (𝓝[s] a ×ˢ pure a) (𝓝[t] g a ×ˢ pure (g a))

pp: case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝[s] a ×ˢ pure a] Prod.map h h

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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Tendsto (Prod.map g g) (𝓝[s] a ×ˢ pure a) (𝓝[t] g a ×ˢ pure (g a))
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr.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 ≠ ∞
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
⊢ 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.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
⊢ 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.Defs

Goal state before:
pp: case e'_10
𝕜 : 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
⊢ (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1)) = fun x ↦ (p' x 0).curry0

pp: case e'_11
𝕜 : 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
⊢ (fun x ↦ ((p' x).unshift (f x)).shift) = p'

Tactic:
·

Goal state after:
case e'_10
𝕜 : 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
⊢ (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1)) = fun x ↦ (p' x 0).curry0
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝[s] a ×ˢ pure a] Prod.map h h

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝[s] a ×ˢ pure a] Prod.map h h
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case e'_11
𝕜 : 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
⊢ (fun x ↦ ((p' x).unshift (f x)).shift) = p'

Tactic:
·

Goal state after:
case e'_11
𝕜 : 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
⊢ (fun x ↦ ((p' x).unshift (f x)).shift) = p'
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Tendsto (Prod.map g g) (𝓝 a ×ˢ pure a) (𝓝 (g a) ×ˢ pure (g a))

pp: case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h

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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Tendsto (Prod.map g g) (𝓝 a ×ˢ pure a) (𝓝 (g a) ×ˢ pure (g a))
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr.refine_3
𝕜 : 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
⊢ n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x i) (v ∩ u)

Tactic:
·

Goal state after:
case mpr.refine_3
𝕜 : 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
⊢ n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (fun x ↦ (p' x).unshift (f x)) x i) (v ∩ u)