awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞
mp :
  HasFPowerSeriesWithinOnBall f p s x r →
    ∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
⊢ HasFPowerSeriesWithinOnBall f p s x r ↔
    ∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
have mpr : (∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r) →
  HasFPowerSeriesWithinOnBall f p s x r
Tactic: constructor
-- 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∞
h : 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 : EqOn f (fun (y : E) ↦ p.sum (y - x)) (insert x s ∩ eball x r)
Tactic: refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
mp : EqOn f (fun (y : E) ↦ p.sum (y - x)) (insert x s ∩ eball x r)
⊢ ∃ (g : E → F), EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
have mp₁ : HasFPowerSeriesOnBall (fun (y : E) ↦ p.sum (y - x)) p x r
Tactic: refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
⊢ y ∈ insert x s ∩ eball x r → f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp : ∀ (ys : y ∈ insert x s) (yb : y ∈ eball x r), f y = (fun (y : E) ↦ p.sum (y - x)) y
Tactic: ⟨ys,yb⟩
-- 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : y ∈ eball x r
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have yb₁ : ‖y - x‖ₑ < r
Tactic: simp only [mem_eball, edist_eq_enorm_sub] at yb
Cleared hypotheses: yb
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp : ∀ (e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))),
  f y = (fun (y : E) ↦ p.sum (y - x)) y
Tactic: have e0 := p.hasSum (x := y - x) ?_
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
mp :
  ∀ (e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))),
    f y = (fun (y : E) ↦ p.sum (y - x)) y
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp₁ : Membership.mem (γ := Set E) (eball 0 p.radius) (y - x)
Tactic: have e0 := p.hasSum (x := y - x) ?_
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp : ∀ (e1 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f (x + (y - x)))),
  f y = (fun (y : E) ↦ p.sum (y - x)) y
Tactic: have e1 := (h.hasSum (y := y - x) ?_ ?_)
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))
mp :
  ∀ (e1 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f (x + (y - x)))),
    f y = (fun (y : E) ↦ p.sum (y - x)) y
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp₁ : x + (y - x) ∈ insert x s
Tactic: have e1 := (h.hasSum (y := y - x) ?_ ?_)
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))
mp :
  ∀ (e1 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f (x + (y - x)))),
    f y = (fun (y : E) ↦ p.sum (y - x)) y
mp₁ : x + (y - x) ∈ insert x s
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have mp₂ : Membership.mem (γ := Set E) (eball 0 r) (y - x)
Tactic: have e1 := (h.hasSum (y := y - x) ?_ ?_)
-- 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (p.sum (y - x))
e1 : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f (x + (y - x)))
⊢ f y = (fun (y : E) ↦ p.sum (y - x)) y
have e1₁ : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
Tactic: simp only [add_sub_cancel] at e1
Cleared hypotheses: e1
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ Membership.mem (γ := Set E) (eball 0 p.radius) (y - x)
have mp : ‖y - x‖ₑ < p.radius
Tactic: simp only [mem_eball, edist_zero_right]
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesOnBall (fun (y : E) ↦ p.sum (y - x)) p x r
have mp : ∀ {y : E},
  Membership.mem (γ := Set E) (eball 0 r) y →
    HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (x + y - x))
Tactic: refine ⟨h.r_le, h.r_pos, ?_⟩
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (x + y - x))
have mp : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
Tactic: simp only [add_sub_cancel_left]
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
have mp : Membership.mem (γ := Set E) (eball 0 p.radius) y
Tactic: apply p.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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ Membership.mem (γ := Set E) (eball 0 p.radius) y
have lt₁ : edist y 0 < r
Tactic: simp only [mem_eball] at lt ⊢
Cleared hypotheses: lt
-- 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∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
⊢ HasFPowerSeriesWithinOnBall f p s x r
have mpr : ∀ {y : E},
  x + y ∈ insert x s →
    Membership.mem (γ := Set E) (eball 0 r) y →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
Tactic: refine ⟨hg.r_le, hg.r_pos, ?_⟩
-- 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∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have mpr : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
Tactic: rw [hfg]
-- 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∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
mpr : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have mpr₁ : x + y ∈ insert x s ∩ eball x r
Tactic: rw [hfg]
-- 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∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ x + y ∈ insert x s ∩ eball x r
have mpr : x + y ∈ eball x r
Tactic: refine ⟨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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ HasFPowerSeriesWithinAt f p s x ↔ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
have mp : HasFPowerSeriesWithinAt f p s x → ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
Tactic: constructor
-- 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
mp : HasFPowerSeriesWithinAt f p s x → ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
⊢ HasFPowerSeriesWithinAt f p s x ↔ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
have mpr : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) → HasFPowerSeriesWithinAt f p s x
Tactic: constructor
-- 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
have mp : ∀ (g : E → F) (e : EqOn f g (insert x s ∩ eball x r)) (h : HasFPowerSeriesOnBall g p x r),
  ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
Tactic: rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨g, e, 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
have mp : f =ᶠ[𝓝[insert x s] x] g
Tactic: refine ⟨g, ?_, ⟨r, 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ f =ᶠ[𝓝[insert x s] x] g
have mp : insert x s ∩ eball x r ∈ 𝓝[insert x s] x
Tactic: refine Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩
-- 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
hfg : f =ᶠ[𝓝[insert x s] x] g
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
⊢ HasFPowerSeriesWithinAt f p s x
have hfg₁ : ∃ ε > 0, ∀ ⦃y : E⦄, dist y x < ε → y ∈ insert x s → f y = g y
Tactic: simp only [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] at hfg
Cleared hypotheses: hfg
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
hfg : ∃ ε > 0, ∀ ⦃y : E⦄, dist y x < ε → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinAt f p s x
have mpr : ∀ (e : ℝ) (e0 : e > 0) (hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y), HasFPowerSeriesWithinAt f p s x
Tactic: rcases hfg with ⟨e, e0, hfg⟩
Cleared hypotheses: hfg
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinAt f p s x
have mpr : HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))
Tactic: refine ⟨min r (.ofReal e), ?_⟩
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))
have mpr : EqOn f g (insert x s ∩ eball x (min r (ENNReal.ofReal e)))
Tactic: refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
mpr : EqOn f g (insert x s ∩ eball x (min r (ENNReal.ofReal e)))
⊢ HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))
have mpr₁ : HasFPowerSeriesOnBall g p x (min r (ENNReal.ofReal e))
Tactic: refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
⊢ y ∈ insert x s ∩ eball x (min r (ENNReal.ofReal e)) → f y = g y
have mpr : ∀ (ys : y ∈ insert x s) (xy : y ∈ eball x (min r (ENNReal.ofReal e))), f y = g y
Tactic: ⟨ys, xy⟩
-- 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ eball x (min r (ENNReal.ofReal e))
⊢ f y = g y
have mpr : dist y x < e
Tactic: refine hfg ?_ 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
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ eball x (min r (ENNReal.ofReal e))
⊢ dist y x < e
have xy₁ : edist y x < r ∧ dist y x < e
Tactic: simp only [mem_eball, lt_min_iff, edist_lt_ofReal] at xy
Cleared hypotheses: xy
-- 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
s : Set E
x : E
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x
have simp : (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
  ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
Tactic: simp only [AnalyticWithinAt, AnalyticAt, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt]
-- 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
s : Set E
x : E
⊢ (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
have mp : (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) →
  ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
Tactic: tauto