awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
⊢ HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) (r - (↑‖y - x‖₊ : ℝ≥0∞))

Tactic:
have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))

Tactic:
simp only [add_sub_cancel] at this

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
apply : r / 2 ≤ r - (↑‖y - x‖₊ : ℝ≥0∞)
⊢ HasFPowerSeriesOnBall f q y (r / 2)

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

Premises used: LT.lt.ne', ENNReal.half_pos, HasFPowerSeriesOnBall.mono, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
apply : (↑‖y - x‖₊ : ℝ≥0∞) + r / 2 ≤ r
⊢ r / 2 ≤ r - (↑‖y - x‖₊ : ℝ≥0∞)

Tactic:
apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top

Premises used: ENNReal.le_sub_of_add_le_left, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
apply : r / 2 + r / 2 = r
⊢ (↑‖y - x‖₊ : ℝ≥0∞) + r / 2 ≤ r

Tactic:
apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)

Premises used: le_refl, add_le_add, HDiv.hDiv, LT.lt.le, LE.le.trans, le_of_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ r / 2 + r / 2 = r

Tactic:
ENNReal.add_halves _

Premises used: ENNReal.add_halves
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ r / 2 + r / 2 = r

Tactic:
exact ENNReal.add_halves _

Premises used: ENNReal.add_halves
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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)
⊢ HasFPowerSeriesOnBall f q y (r / 2)

Tactic:
have has_series : HasFPowerSeriesOnBall f q y (r / 2) := by
    have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
    have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
    simp only [add_sub_cancel] at this
    apply this.mono (ENNReal.half_pos hp.r_pos.ne')
    apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top
    apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)
    exact ENNReal.add_halves _
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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)
⊢ Metric.eball y (r / 2) ∈ 𝓝 x

Tactic:
have M : Metric.eball y (r / 2) ∈ 𝓝 x := Metric.isOpen_eball.mem_nhds hxy
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
h : ∀ (z : E) (hz : z ∈ Metric.eball y (r / 2)), f z = 0 z
⊢ x ∈ u

Tactic:
filter_upwards [M] with z hz
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
⊢ HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)

Tactic:
have A : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) (f z) := has_series.hasSum_sub hz
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
⊢ HasFPowerSeriesAt 0 q y

Tactic:
have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ HasSum.{u_3, 0} (α := F) (fun (x : ℕ) ↦ 0) 0

Tactic:
hasSum_zero (α := F)

Premises used: hasSum_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
h : Eq.{u_3 + 1} (α := ℕ → F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) fun (x : ℕ) ↦ 0
⊢ HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0

Tactic:
convert! hasSum_zero (α := F) using 1

Premises used: hasSum_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
h : ∀ (n : ℕ), Eq.{u_3 + 1} (α := F) ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := ℕ → F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) fun (x : ℕ) ↦ 0

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
n : ℕ
⊢ Eq.{u_3 + 1} (α := F) ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y : F) (0 : F)

Tactic:
this.apply_eq_zero n _

Premises used: HasFPowerSeriesAt.apply_eq_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
n : ℕ
⊢ Eq.{u_3 + 1} (α := F) ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y : F) (0 : F)

Tactic:
exact this.apply_eq_zero n _

Premises used: HasFPowerSeriesAt.apply_eq_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
⊢ HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0

Tactic:
have B : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) 0 := by
    have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
    convert! hasSum_zero (α := F) using 1
    ext n
    exact this.apply_eq_zero n _
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
B : HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0
⊢ f z = 0 z

Tactic:
HasSum.unique A B

Premises used: HasSum.unique
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : 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 : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
B : HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0
⊢ f z = 0 z

Tactic:
exact HasSum.unique A B

Premises used: HasSum.unique
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
⊢ AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U

Tactic:
have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
apply : (𝓝 z₀).EventuallyEq (β := F') ((⇑e : (a : F) → F') ∘ f) 0
⊢ EqOn (β := F') ((⇑e : (a : F) → F') ∘ f) 0 U

Tactic:
apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
h : ∀ (x : E) (hx : f x = 0 x), Eq (α := F') (((⇑e : (a : F) → F') ∘ f) x) (0 x)
⊢ (𝓝 z₀).EventuallyEq (β := F') ((⇑e : (a : F) → F') ∘ f) 0

Tactic:
filter_upwards [hfz₀] with x hx
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
x : E
hx : f x = 0 x
⊢ Eq (α := F') (((⇑e : (a : F) → F') ∘ f) x) (0 x)

Tactic:
simp only [hx, Function.comp_apply, Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero, Function.comp_apply
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
⊢ EqOn (β := F') ((⇑e : (a : F) → F') ∘ f) 0 U

Tactic:
have A : EqOn (e ∘ f) 0 U := by
    apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀
    filter_upwards [hfz₀] with x hx
    simp only [hx, Function.comp_apply, Pi.zero_apply, map_zero]
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
A : EqOn (β := F') ((⇑e : (a : F) → F') ∘ f) 0 U
z : E
hz : z ∈ U
⊢ Eq (α := F') ((e : (a : F) → F') (f z) : F') ((e : (a : F) → F') 0 : F')

Tactic:
simpa only using A hz