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
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:
have : e (f z) = e 0 := by simpa only using A 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
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_1 : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
A : EqOn (β := F') ((⇑e : (a : F) → F') ∘ f) 0 U
z : E
hz : z ∈ U
this : Eq (α := F') ((e : (a : F) → F') (f z) : F') ((e : (a : F) → F') 0 : F')
⊢ f z = 0 z

Tactic:
UniformSpace.Completion.coe_injective F this

Premises used: UniformSpace.Completion.coe_injective
-- 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_1 : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
A : EqOn (β := F') ((⇑e : (a : F) → F') ∘ f) 0 U
z : E
hz : z ∈ U
this : Eq (α := F') ((e : (a : F) → F') (f z) : F') ((e : (a : F) → F') 0 : F')
⊢ f z = 0 z

Tactic:
exact UniformSpace.Completion.coe_injective F this

Premises used: UniformSpace.Completion.coe_injective
-- 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 g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
z : E
h : f z = g z
⊢ (f - g) z = 0 z

Tactic:
simp [h]
-- 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 g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
⊢ f - g =ᶠ[𝓝 z₀] 0

Tactic:
have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]
-- 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 g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
hfg' : f - g =ᶠ[𝓝 z₀] 0
⊢ EqOn f g U

Tactic:
simpa [sub_eq_zero] using fun z hz =>
    (hf.sub hg).eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀ hfg' hz

Premises used: sub_eq_zero, AnalyticOnNhd.sub, AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_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 g : E → F
inst_5 : PreconnectedSpace E
hf : AnalyticOnNhd 𝕜 f univ
hg : AnalyticOnNhd 𝕜 g univ
z₀ : E
hfg : f =ᶠ[𝓝 z₀] g
⊢ f = g

Tactic:
funext fun x =>
    eqOn_of_preconnected_of_eventuallyEq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)

Premises used: funext, Set.mem_univ, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Analytic.WithLp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
p : ℝ≥0∞
inst_5 : Fact (1 ≤ p)
s : Set (WithLp p (E × F))
⊢ AnalyticOn 𝕜 ofLp s

Tactic:
(prodContinuousLinearEquiv p 𝕜 E F).analyticOn s

Premises used: WithLp.prodContinuousLinearEquiv, ContinuousLinearEquiv.analyticOn
-- Module: Mathlib.Analysis.Analytic.WithLp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
p : ℝ≥0∞
inst_5 : Fact (1 ≤ p)
s : Set (E × F)
⊢ AnalyticOn 𝕜 (toLp p) s

Tactic:
(prodContinuousLinearEquiv p 𝕜 E F).symm.analyticOn s

Premises used: ContinuousLinearEquiv.symm, WithLp.prodContinuousLinearEquiv, ContinuousLinearEquiv.analyticOn
-- Module: Mathlib.Analysis.Analytic.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
s : Set (PiLp p E)
⊢ AnalyticOn 𝕜 ofLp s

Tactic:
(continuousLinearEquiv p 𝕜 E).analyticOn s

Premises used: ContinuousLinearEquiv.analyticOn, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Analytic.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
s : Set ((i : ι) → E i)
⊢ AnalyticOn 𝕜 (toLp p) s

Tactic:
(continuousLinearEquiv p 𝕜 E).symm.analyticOn s

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.analyticOn, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
rcases :
  ∀ (t : Set E) (ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (xt : x ∈ t) (st : t ∩ s ⊆ {x}),
    AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
rcases : ∀ (r : ℝ) (r0 : r > 0) (rt : ball x r ⊆ t), AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases Metric.mem_nhds_iff.mp (ot.mem_nhds xt) with ⟨r, r0, rt⟩

Premises used: Metric.mem_nhds_iff, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
⊢ ENNReal.ofReal r ≤ FormalMultilinearSeries.radius (constFormalMultilinearSeries 𝕜 E (f x))

Tactic:
simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]

Premises used: le_top, FormalMultilinearSeries.constFormalMultilinearSeries_radius
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
⊢ ∀ y ∈ t, y ∈ s → y = x

Tactic:
simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st

Premises used: Set.subset_singleton_iff, and_imp, Set.mem_inter_iff
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
⊢ y = 0 ∨ x + y ∈ s

Tactic:
simp only [mem_insert_iff, add_eq_left] at ys

Premises used: add_eq_left, Set.mem_insert_iff
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
inl : ∀ (yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) 0), x + 0 = x
inr : ∀ (ys : x + y ∈ s), x + y = x
⊢ x + y = x

Tactic:
rcases ys with rfl | ys

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
st : ∀ y ∈ t, y ∈ s → y = x
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) 0
⊢ x + 0 = x

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y ∈ ball x r

Tactic:
simpa using yr
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x

Tactic:
exact st (x + y) (rt (by simpa using yr)) ys

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
⊢ x + y = x

Tactic:
have : x + y = x := by
        rcases ys with rfl | ys
        · simp
        · exact st (x + y) (rt (by simpa using yr)) ys
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
this : x + y = x
simp :
  HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f x)
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f (x + y))

Tactic:
simp only [this]
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
this : x + y = x
apply : Membership.mem (γ := Set E) (eball 0 ∞) y
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f x)

Tactic:
apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum

Premises used: hasFPowerSeriesOnBall_const, HasFPowerSeriesOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) y
st : ∀ y ∈ t, y ∈ s → y = x
ys : y = 0 ∨ x + y ∈ s
this : x + y = x
⊢ Membership.mem (γ := Set E) (eball 0 ∞) y

Tactic:
simp only [eball_top, mem_univ]

Premises used: Metric.eball_top, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact ⟨constFormalMultilinearSeries 𝕜 E (f x), .ofReal r,
  { r_le := by simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]
    r_pos := by positivity
    hasSum := by
      intro y ys yr
      simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st
      simp only [mem_insert_iff, add_eq_left] at ys
      have : x + y = x := by
        rcases ys with rfl | ys
        · simp
        · exact st (x + y) (rt (by simpa using yr)) ys
      simp only [this]
      apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum
      simp only [eball_top, mem_univ] }⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
rcases :
  ∀ (u : Set E) (ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
    (fu : AnalyticOn 𝕜 f (s ∩ u)), AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases h x m with ⟨u, ou, xu, fu⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
rcases : ∀ (r : ℝ) (r0 : r > 0) (ru : ball x r ⊆ u), AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩

Premises used: Metric.mem_nhds_iff, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (t : ℝ≥0∞) (fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t),
    AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

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

Premises used: And.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : Membership.mem (γ := Set E) (eball 0 (min (ENNReal.ofReal r) t)) y
⊢ ‖y‖ < r ∧ edist y 0 < t

Tactic:
simp only [mem_eball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr

Premises used: edist_lt_ofReal, dist_zero_right, lt_min_iff, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
a : x + y ∈ insert x (s ∩ u)
a₁ : Membership.mem (γ := Set E) (eball 0 t) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
apply fp.hasSum

Premises used: HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ y = 0 ∨ x + y ∈ s

Tactic:
simp only [mem_insert_iff, add_eq_left] at ys

Premises used: add_eq_left, Set.mem_insert_iff
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : y = 0 ∨ x + y ∈ s
a : ∀ (yr : norm.{u_2} (E := E) 0 < r ∧ edist.{u_2} (α := E) 0 0 < t), x + 0 ∈ insert x (s ∩ u)
a₁ : ∀ (ys : x + y ∈ s), x + y ∈ insert x (s ∩ u)
⊢ x + y ∈ insert x (s ∩ u)

Tactic:
rcases ys with rfl | ys

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
yr : norm.{u_2} (E := E) 0 < r ∧ edist.{u_2} (α := E) 0 0 < t
⊢ x + 0 ∈ insert x (s ∩ u)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h :
  ∀ x ∈ s, ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
a : y = 0 ∨ x + y ∈ u
⊢ x + y ∈ insert x (s ∩ u)

Tactic:
simp only [mem_insert_iff, add_eq_left, mem_inter_iff, ys, true_and]

Premises used: Set.mem_inter_iff, add_eq_left, Set.mem_insert_iff, true_and