awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
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
have apply : (𝓝 z₀).EventuallyEq (β := F') ((⇑e : (a : F) → F') ∘ f) 0
Tactic: apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
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
⊢ (𝓝 z₀).EventuallyEq (β := F') ((⇑e : (a : F) → F') ∘ f) 0
have h : ∀ (x : E) (hx : f x = 0 x), Eq (α := F') (((⇑e : (a : F) → F') ∘ f) x) (0 x)
Tactic: filter_upwards [hfz₀] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (hypothesis)
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 0 U
have A : 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (hypothesis)
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
⊢ f z = 0 z
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (hypothesis)
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
⊢ EqOn f g U
have hfg' : f - g =ᶠ[𝓝 z₀] 0
Tactic: have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (t : Set E) (ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (xt : x ∈ t) (st : t ∩ s ⊆ {x}),
  AnalyticWithinAt 𝕜 f s x
Tactic: rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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}
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (r : ℝ) (r0 : r > 0) (rt : ball x r ⊆ t), AnalyticWithinAt 𝕜 f s x
Tactic: rcases Metric.mem_nhds_iff.mp (ot.mem_nhds xt) with ⟨r, r0, rt⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f (x + y))
have st₁ : ∀ y ∈ t, y ∈ s → y = x
Tactic: simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st
Cleared hypotheses: st
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f (x + y))
have ys₁ : y = 0 ∨ x + y ∈ s
Tactic: simp only [mem_insert_iff, add_eq_left] at ys
Cleared hypotheses: ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
have inl : ∀ (yr : Membership.mem (γ := Set E) (eball 0 (ENNReal.ofReal r)) 0), x + 0 = x
Tactic: rcases ys with rfl | ys
Cleared hypotheses: y, yr, ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ x + y = x
have inr : ∀ (ys : x + y ∈ s), x + y = x
Tactic: rcases ys with rfl | ys
Cleared hypotheses: ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f (x + y))
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f (x + y))
have simp : HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f x)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ HasSum (fun (n : ℕ) ↦ (constFormalMultilinearSeries 𝕜 E (f x) n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (f x)
have apply : Membership.mem (γ := Set E) (eball 0 ∞) y
Tactic: apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (u : Set E) (ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (fu : AnalyticOn 𝕜 f (s ∩ u)), AnalyticWithinAt 𝕜 f s x
Tactic: rcases h x m with ⟨u, ou, xu, fu⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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)
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (r : ℝ) (r0 : r > 0) (ru : ball x r ⊆ u), AnalyticWithinAt 𝕜 f s x
Tactic: rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (t : ℝ≥0∞) (fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t),
  AnalyticWithinAt 𝕜 f s x
Tactic: rcases fu x ⟨m, xu⟩ with ⟨p, t, fp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have yr₁ : ‖y‖ < r ∧ edist y 0 < t
Tactic: simp only [mem_eball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr
Cleared hypotheses: yr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have a : x + y ∈ insert x (s ∩ u)
Tactic: apply fp.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have a₁ : Membership.mem (γ := Set E) (eball 0 t) y
Tactic: apply fp.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
⊢ x + y ∈ insert x (s ∩ u)
have ys₁ : y = 0 ∨ x + y ∈ s
Tactic: simp only [mem_insert_iff, add_eq_left] at ys
Cleared hypotheses: ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ x + y ∈ insert x (s ∩ u)
have a : ∀ (yr : norm.{u_2} (E := E) 0 < r ∧ edist.{u_2} (α := E) 0 0 < t), x + 0 ∈ insert x (s ∩ u)
Tactic: rcases ys with rfl | ys
Cleared hypotheses: y, yr, ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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)
⊢ x + y ∈ insert x (s ∩ u)
have a₁ : ∀ (ys : x + y ∈ s), x + y ∈ insert x (s ∩ u)
Tactic: rcases ys with rfl | ys
Cleared hypotheses: ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ x + y ∈ insert x (s ∩ u)
have a : y = 0 ∨ x + y ∈ u
Tactic: simp only [mem_insert_iff, add_eq_left, mem_inter_iff, ys, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
⊢ y = 0 ∨ x + y ∈ u
have apply : x + y ∈ ball x r
Tactic: apply Or.inr (ru ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s
have refine : AnalyticOn 𝕜 f s → AnalyticOnNhd 𝕜 f s
Tactic: refine ⟨?_, AnalyticOnNhd.analyticOn⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
⊢ AnalyticAt 𝕜 f x
have rcases : ∀ (r : ℝ) (r0 : r > 0) (rs : ball x r ⊆ s), AnalyticAt 𝕜 f x
Tactic: rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
⊢ AnalyticAt 𝕜 f x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (t : ℝ≥0∞) (fp : HasFPowerSeriesWithinOnBall f p s x t), AnalyticAt 𝕜 f x
Tactic: rcases hf x m with ⟨p, t, fp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : Membership.mem (γ := Set E) (eball 0 (min (ENNReal.ofReal r) t)) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have ym₁ : ‖y‖ < r ∧ edist y 0 < t
Tactic: simp only [mem_eball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
Cleared hypotheses: ym
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have refine : x + y ∈ insert x s
Tactic: refine fp.hasSum ?_ ym.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ insert x s
have a : x + y ∈ s
Tactic: apply mem_insert_of_mem
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ s
have a : x + y ∈ ball x r
Tactic: apply rs
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p s x r ↔
    ∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
have mp : HasFPowerSeriesWithinOnBall f p s x r → ∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
Tactic: constructor