-- Mathlib/Analysis/Analytic/Within.lean
/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide -/
lemma IsOpen.analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen s) :
    AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Proof state:
case a
𝕜 : 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ s

Tactic:
apply rs

Result:
case a.a
𝕜 : 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ Metric.ball x r

Proof state:
case intro.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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ AnalyticAt 𝕜 f x

Tactic:
exact ⟨p, min (.ofReal r) t,
{ r_pos := lt_min (by positivity) fp.r_pos
  r_le := min_le_of_right_le fp.r_le
  hasSum := by
    intro y ym
    simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
    refine fp.hasSum ?_ ym.2
    apply mem_insert_of_mem
    apply rs
    simp only [Metric.mem_ball, dist_self_add_left, ym.1] }⟩

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
hs : IsOpen s
⊢ AnalyticOn 𝕜 f s → AnalyticOnNhd 𝕜 f s

Tactic:
intro hf x m

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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
⊢ AnalyticAt 𝕜 f 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
refine fp.hasSum ?_ ym.2

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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ insert x s

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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩

Result:
case 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
⊢ AnalyticAt 𝕜 f x

Proof state:
case 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases hf x m with ⟨p, t, fp⟩

Result:
case intro.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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ AnalyticAt 𝕜 f 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
hs : IsOpen s
⊢ AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Tactic:
refine ⟨?_, AnalyticOnNhd.analyticOn⟩

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
hs : IsOpen s
⊢ AnalyticOn 𝕜 f s → AnalyticOnNhd 𝕜 f s

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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ ∀ {y : E}, y ∈ EMetric.ball 0 (ENNReal.ofReal r ⊓ t) → HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
intro y ym

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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : y ∈ EMetric.ball 0 (ENNReal.ofReal r ⊓ t)
⊢ HasSum (fun n => (p n) fun x => y) (f (x + y))

Proof state:
case a.a
𝕜 : 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
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ Metric.ball x r

Tactic:
simp only [Metric.mem_ball, dist_self_add_left, ym.1]

Result:
no goals