-- Mathlib/Analysis/Analytic/Within.lean
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
version, we make sure that the extension coincides with `f` on all of `insert x s`. -/
lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
    AnalyticWithinAt 𝕜 f s x ↔
      ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Proof state:
case refine_1.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
⊢ ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩

Result:
case refine_1.intro.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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
⊢ ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Proof state:
case refine_1.intro.intro.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
⊢ f x = g' x

Tactic:
have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩

Result:
case refine_1.intro.intro.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
this : x ∈ u ∩ insert x s
⊢ f x = g' x

Proof state:
case refine_1.intro.intro.intro.intro.intro.refine_3
𝕜 : 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
⊢ g =ᶠ[𝓝 x] g'

Tactic:
filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]

Result:
no goals

Proof state:
case pos
𝕜 : 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∈ u
this : y ∈ u ∩ insert x s
⊢ f y = g' y

Tactic:
simpa [g', h'y, this] using hu this

Result:
no goals

Proof state:
case refine_1.intro.intro.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
this : x ∈ u ∩ insert x s
⊢ f x = g' x

Tactic:
simpa [g', xu, this] using hu this

Result:
no goals

Proof state:
case 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
⊢ (∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
rintro ⟨g, -, hf, hg⟩

Result:
case refine_2.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
g : E → F
hf : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Proof state:
case neg
𝕜 : 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∉ u
⊢ f y = g' y

Tactic:
simp [g', h'y]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.refine_3
𝕜 : 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
⊢ AnalyticAt 𝕜 g' x

Tactic:
apply hg.congr

Result:
case refine_1.intro.intro.intro.intro.intro.refine_3
𝕜 : 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
⊢ g =ᶠ[𝓝 x] g'

Proof state:
case refine_1.intro.intro.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
⊢ EqOn f g' (insert x s)

Tactic:
intro y hy

Result:
case refine_1.intro.intro.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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
⊢ f y = g' y