-- Mathlib/Analysis/Analytic/Within.lean
/-- `AnalyticWithinAt` is trivial if `{x} ∈ 𝓝[s] x` -/
lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : {x} ∈ 𝓝[s] x) :
    AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
⊢ x + y = x

Tactic:
rcases ys with rfl | ys

Result:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
st : ∀ y ∈ t, y ∈ s → y = x
yr : 0 ∈ EMetric.ball 0 (ENNReal.ofReal r)
⊢ x + 0 = x

case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x

Proof state:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
st : ∀ y ∈ t, y ∈ s → y = x
yr : 0 ∈ EMetric.ball 0 (ENNReal.ofReal r)
⊢ x + 0 = x

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
⊢ ENNReal.ofReal r ≤ (constFormalMultilinearSeries 𝕜 E (f x)).radius

Tactic:
simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f (x + y))

Tactic:
simp only [mem_insert_iff, add_right_eq_self] at ys

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f (x + y))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y ∈ Metric.ball x r

Tactic:
simpa using yr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f (x + y))

Tactic:
simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f (x + y))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
this : x + y = x
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f (x + y))

Tactic:
simp only [this]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
this : x + y = x
⊢ HasSum (fun n => (constFormalMultilinearSeries 𝕜 E (f x) n) fun x => y) (f x)

Proof state:
case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
y : E
yr : y ∈ EMetric.ball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x

Tactic:
exact st (x + y) (rt (by simpa using yr)) ys

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : Metric.ball x r ⊆ t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen t
xt : x ∈ t
st : t ∩ s ⊆ {x}
⊢ AnalyticWithinAt 𝕜 f s x