-- Mathlib/Analysis/Analytic/Within.lean
lemma AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn
    [CompleteSpace F] {f : E → F} {s : Set E} {x : E} (h : AnalyticWithinAt 𝕜 f s x) :
    ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Proof state:
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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
refine ⟨u, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ u ∈ 𝓝[insert x s] x

case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ AnalyticOn 𝕜 f u

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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
obtain ⟨g, -, h'g, hg⟩ : ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x :=
  h.exists_analyticAt

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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Proof state:
case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
⊢ AnalyticWithinAt 𝕜 f u y

Tactic:
have : AnalyticWithinAt 𝕜 g u y := hy.2.analyticWithinAt

Result:
case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
this : AnalyticWithinAt 𝕜 g u y
⊢ AnalyticWithinAt 𝕜 f u y

Proof state:
case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
this : AnalyticWithinAt 𝕜 g u y
⊢ AnalyticWithinAt 𝕜 f u y

Tactic:
exact this.congr (h'g.mono (inter_subset_left)) (h'g (inter_subset_left hy))

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ u ∈ 𝓝[insert x s] x

Tactic:
exact inter_mem_nhdsWithin _ ((isOpen_analyticAt 𝕜 g).mem_nhds hg)

Result:
no goals

Proof state:
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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
let u := insert x s ∩ {y | AnalyticAt 𝕜 g y}

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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Proof state:
case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ AnalyticOn 𝕜 f u

Tactic:
intro y hy

Result:
case intro.intro.intro.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
⊢ AnalyticWithinAt 𝕜 f u y