case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : none + 1 ≤ n
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s

case some
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hmn : some m + 1 ≤ n
⊢ ContDiffOn 𝕜 (some m) (fun y => fderivWithin 𝕜 f s y) 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
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (fun y => fderivWithin 𝕜 f s y) s
cases' m with m
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : none + 1 ≤ n
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
change ∞ + 1 ≤ n at hmn
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
this : n = ⊤
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
have : n = ∞ := by simpa using hmn
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 ⊤ f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
this : n = ⊤
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
this : n = ⊤
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
rw [this] at hf
no goals
case none
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 ⊤ f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
this : n = ⊤
⊢ ContDiffOn 𝕜 none (fun y => fderivWithin 𝕜 f s y) s
exact ((contDiffOn_top_iff_fderivWithin hs).1 hf).2
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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : ⊤ + 1 ≤ n
⊢ n = ⊤
simpa using hmn
case some
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hmn : ↑(Nat.succ m) ≤ n
⊢ ContDiffOn 𝕜 (some m) (fun y => fderivWithin 𝕜 f s y) s
case some
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hmn : some m + 1 ≤ n
⊢ ContDiffOn 𝕜 (some m) (fun y => fderivWithin 𝕜 f s y) s
change (m.succ : ℕ∞) ≤ n at hmn
no goals
case some
𝕜 : 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
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hmn : ↑(Nat.succ m) ≤ n
⊢ ContDiffOn 𝕜 (some m) (fun y => fderivWithin 𝕜 f s y) s
exact ((contDiffOn_succ_iff_fderivWithin hs).1 (hf.of_le hmn)).2