-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f : E → F} {U : Set E}
    (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
    {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
    EqOn f 0 U

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : ↑‖y - x‖₊ < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)
⊢ r / 2 ≤ r - ↑‖y - x‖₊

Tactic:
apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : ↑‖y - x‖₊ < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)
⊢ ↑‖y - x‖₊ + r / 2 ≤ r

Proof state:
case h.e.h.e'_5.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : EMetric.ball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ EMetric.ball y (r / 2)
A : HasSum (fun n => (q n) fun x => z - y) (f z)
this : HasFPowerSeriesAt 0 q y
n : ℕ
⊢ ((q n) fun x => z - y) = 0

Tactic:
exact this.apply_eq_zero n _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : ↑‖y - x‖₊ < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)
⊢ HasFPowerSeriesOnBall f q y (r / 2)

Tactic:
apply this.mono (ENNReal.half_pos hp.r_pos.ne')

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : ↑‖y - x‖₊ < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)
⊢ r / 2 ≤ r - ↑‖y - x‖₊

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : EMetric.ball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ EMetric.ball y (r / 2)
A : HasSum (fun n => (q n) fun x => z - y) (f z)
⊢ HasSum (fun n => (q n) fun x => z - y) 0

Tactic:
have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : EMetric.ball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ EMetric.ball y (r / 2)
A : HasSum (fun n => (q n) fun x => z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ HasSum (fun n => (q n) fun x => z - y) 0

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : EMetric.ball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ EMetric.ball y (r / 2)
A : HasSum (fun n => (q n) fun x => z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ HasSum (fun n => (q n) fun x => z - y) 0

Tactic:
convert hasSum_zero (α := F) using 2

Result:
case h.e.h.e'_5
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : EMetric.ball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ EMetric.ball y (r / 2)
A : HasSum (fun n => (q n) fun x => z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ (fun n => (q n) fun x => z - y) = fun x => 0