case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s →
    (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
          (fun x => FormalMultilinearSeries.shift (p x)) s

case mpr
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
          (fun x => FormalMultilinearSeries.shift (p x)) s →
    HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s ↔
    (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
          (fun x => FormalMultilinearSeries.shift (p x)) s
constructor
case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
    (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
      HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
        (fun x => FormalMultilinearSeries.shift (p x)) s
case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s →
    (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
          (fun x => FormalMultilinearSeries.shift (p x)) s
intro H
case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
    (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
      HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
        (fun x => FormalMultilinearSeries.shift (p x)) s
refine' ⟨H.zero_eq, H.fderivWithin 0 (Nat.cast_lt.2 (Nat.succ_pos n)), _⟩
no goals
case mp
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
exact H.shift_of_succ
case mpr.intro.intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
case mpr
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
          (fun x => FormalMultilinearSeries.shift (p x)) s →
    HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
rintro ⟨Hzero_eq, Hfderiv_zero, Htaylor⟩
case mpr.intro.intro.zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x

case mpr.intro.intro.fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (m : ℕ),
    ↑m < ↑(n + 1) →
      ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun x => p x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x

case mpr.intro.intro.cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑(n + 1) → ContinuousOn (fun x => p x m) s
case mpr.intro.intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
constructor
no goals
case mpr.intro.intro.zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
exact Hzero_eq
case mpr.intro.intro.fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑m < ↑(Nat.succ n)
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => p x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x
case mpr.intro.intro.fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (m : ℕ),
    ↑m < ↑(n + 1) →
      ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun x => p x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x
intro m (hm : (m : ℕ∞) < n.succ) x (hx : x ∈ s)
case mpr.intro.intro.fderivWithin.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
hm : ↑Nat.zero < ↑(Nat.succ n)
⊢ HasFDerivWithinAt (fun x => p x Nat.zero) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ Nat.zero))) s x

case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
case mpr.intro.intro.fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑m < ↑(Nat.succ n)
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => p x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x
cases' m with m
no goals
case mpr.intro.intro.fderivWithin.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
hm : ↑Nat.zero < ↑(Nat.succ n)
⊢ HasFDerivWithinAt (fun x => p x Nat.zero) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ Nat.zero))) s x
exact Hfderiv_zero x hx
case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
have A : (m : ℕ∞) < n := by
  rw [Nat.cast_lt] at hm ⊢
  exact Nat.lt_of_succ_lt_succ hm
case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt
    (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) ∘ fun x => p x (Nat.succ m))
    (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))) s x
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'] at this
case h.e'_10.h.h
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
⊢ ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m))) =
    ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m)))
case mpr.intro.intro.fderivWithin.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
⊢ HasFDerivWithinAt (fun x => p x (Nat.succ m)) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) s x
convert this
case h.e'_10.h.h.h.H
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
y : E
v : Fin (Nat.succ m) → E
⊢ ↑(↑(ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) y) v =
    ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk
                  (LinearIsometryEquiv.symm
                      (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
              (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
          y)
      v
case h.e'_10.h.h
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
⊢ ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m))) =
    ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m)))
ext (y v)
case h.e'_10.h.h.h.H
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
y : E
v : Fin (Nat.succ m) → E
⊢ ↑(p x (Nat.succ (Nat.succ m))) (cons y v) = ↑(p x (Nat.succ (Nat.succ m))) (snoc (cons y (init v)) (v (last m)))
case h.e'_10.h.h.h.H
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
y : E
v : Fin (Nat.succ m) → E
⊢ ↑(↑(ContinuousMultilinearMap.curryLeft (p x (Nat.succ (Nat.succ m)))) y) v =
    ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk
                  (LinearIsometryEquiv.symm
                      (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
              (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
          y)
      v
change
  (p x (Nat.succ (Nat.succ m))) (cons y v) =
    (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))
no goals
case h.e'_10.h.h.h.H
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x (Nat.succ m))
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F))).toLinearEquiv))
      (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.shift (p x) (Nat.succ m))))
    s x
e_7✝ : ContinuousMultilinearMap.normedAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'
y : E
v : Fin (Nat.succ m) → E
⊢ ↑(p x (Nat.succ (Nat.succ m))) (cons y v) = ↑(p x (Nat.succ (Nat.succ m))) (snoc (cons y (init v)) (v (last m)))
rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : Nat.succ m < Nat.succ n
⊢ m < n
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(Nat.succ m) < ↑(Nat.succ n)
⊢ ↑m < ↑n
rw [Nat.cast_lt] at hm ⊢
no goals
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
x : E
hx : x ∈ s
m : ℕ
hm : Nat.succ m < Nat.succ n
⊢ m < n
exact Nat.lt_of_succ_lt_succ hm
case mpr.intro.intro.cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑m ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x m) s
case mpr.intro.intro.cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑(n + 1) → ContinuousOn (fun x => p x m) s
intro m (hm : (m : ℕ∞) ≤ n.succ)
case mpr.intro.intro.cont.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
hm : ↑Nat.zero ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x Nat.zero) s

case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x (Nat.succ m)) s
case mpr.intro.intro.cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑m ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x m) s
cases' m with m
case mpr.intro.intro.cont.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
hm : ↑Nat.zero ≤ ↑(Nat.succ n)
this : DifferentiableOn 𝕜 (fun x => p x 0) s
⊢ ContinuousOn (fun x => p x Nat.zero) s
case mpr.intro.intro.cont.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
hm : ↑Nat.zero ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x Nat.zero) s
have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
  (Hfderiv_zero x hx).differentiableWithinAt
no goals
case mpr.intro.intro.cont.zero
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
hm : ↑Nat.zero ≤ ↑(Nat.succ n)
this : DifferentiableOn 𝕜 (fun x => p x 0) s
⊢ ContinuousOn (fun x => p x Nat.zero) s
exact this.continuousOn
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ContinuousOn (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) ∘ fun x => p x (Nat.succ m))
    s
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ContinuousOn (fun x => p x (Nat.succ m)) s
refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm.comp_continuousOn_iff.mp ?_
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ↑m ≤ ↑n
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ContinuousOn (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) ∘ fun x => p x (Nat.succ m))
    s
refine Htaylor.cont _ ?_
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : Nat.succ m ≤ Nat.succ n
⊢ m ≤ n
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : ↑(Nat.succ m) ≤ ↑(Nat.succ n)
⊢ ↑m ≤ ↑n
rw [Nat.cast_le] at hm ⊢
no goals
case mpr.intro.intro.cont.succ
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (p x 0) = f x
Hfderiv_zero : ∀ (x : E), x ∈ s → HasFDerivWithinAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1))
    (fun x => FormalMultilinearSeries.shift (p x)) s
m : ℕ
hm : Nat.succ m ≤ Nat.succ n
⊢ m ≤ n
exact Nat.lt_succ_iff.mp hm