-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesWithinOnBall.differentiableOn [CompleteSpace F]
    (h : HasFPowerSeriesWithinOnBall f p s x r) :
    DifferentiableOn 𝕜 f (insert x s ∩ EMetric.ball x r)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Tactic:
have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ DifferentiableOn 𝕜 f (insert x s ∩ EMetric.ball x r)

Tactic:
intro y hy

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s ∩ EMetric.ball x r] y

Tactic:
suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this

Result:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s] y

Proof state:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
s : Set E
inst✝ : CompleteSpace F
y : E
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
h : HasFPowerSeriesWithinOnBall f p s y r
hy : y ∈ insert y s ∩ EMetric.ball y r
⊢ DifferentiableWithinAt 𝕜 f (insert y s ∩ EMetric.ball y r) y

Tactic:
exact Z.mono inter_subset_left

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s] y

Tactic:
rw [nhdsWithin_insert_of_ne hy]

Result:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y

Tactic:
exact self_mem_nhdsWithin

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Tactic:
rcases eq_or_ne y x with rfl | hy

Result:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
s : Set E
inst✝ : CompleteSpace F
y : E
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
h : HasFPowerSeriesWithinOnBall f p s y r
hy : y ∈ insert y s ∩ EMetric.ball y r
⊢ DifferentiableWithinAt 𝕜 f (insert y s ∩ EMetric.ball y r) y

case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ EMetric.ball x r) y

Tactic:
apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin

Result:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ EMetric.ball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s ∩ EMetric.ball x r] y