awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : y = 0 ∨ x + y ∈ s
⊢ g (x + y) = f (x + y)
have h₁ : ∀ (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) 0), g (x + 0) = f (x + 0)
Tactic: rcases hy with rfl | hy
Cleared hypotheses: y, h'y, hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : y = 0 ∨ x + y ∈ s
h₁ : ∀ (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) 0), g (x + 0) = f (x + 0)
⊢ g (x + y) = f (x + y)
have h₂ : ∀ (hy : x + y ∈ s), g (x + y) = f (x + y)
Tactic: rcases hy with rfl | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
⊢ g (x + y) = f (x + y)
have h₁ : x + y ∈ s ∩ Metric.eball x r
Tactic: apply h'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
⊢ x + y ∈ s ∩ Metric.eball x r
have h₁ : x + y ∈ Metric.eball x r
Tactic: refine ⟨hy, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
⊢ HasFPowerSeriesWithinOnBall g p s x r
have refine : ∀ {y : E} (hy : x + y ∈ insert x s) (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
  HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
Tactic: refine ⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
have h₁ : g (x + y) = f (x + y)
Tactic: convert! h.hasSum hy h'y using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h : HasFPowerSeriesWithinAt f p s x
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
⊢ HasFPowerSeriesWithinAt g p s x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r), HasFPowerSeriesWithinAt g p s x
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt g p s x
have obtain : ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}), HasFPowerSeriesWithinAt g p s x
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, Metric.eball x ε ∩ s ⊆ {y | g y = f y} :=
    EMetric.mem_nhdsWithin_iff.1 h'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinAt g p s x
have refine : HasFPowerSeriesWithinOnBall g p s x r'
Tactic: refine ⟨r', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinOnBall g p s x r'
have this : HasFPowerSeriesWithinOnBall f p s x r'
Tactic: have := hr.of_le (r' := r') (by simp [r', εpos, hr.r_pos]) (min_le_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}
r' : ℝ≥0∞ := min r ε
this : HasFPowerSeriesWithinOnBall f p s x r'
⊢ HasFPowerSeriesWithinOnBall g p s x r'
have apply : EqOn g f (s ∩ Metric.eball x r')
Tactic: apply this.congr _ h''
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
have h : g (x + y) = f (x + y)
Tactic: convert! hf.hasSum hy using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ g (x + y) = f (x + y)
have h : x + y ∈ Metric.eball x r
Tactic: apply hg.symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
hg : f =ᶠ[𝓝 x] g
⊢ HasFPowerSeriesAt g p x
have rcases : ∀ (r₁ : ℝ≥0∞) (h₁ : HasFPowerSeriesOnBall f p x r₁), HasFPowerSeriesAt g p x
Tactic: rcases hf with ⟨r₁, h₁⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
⊢ HasFPowerSeriesAt g p x
have rcases : ∀ (r₂ : ℝ≥0∞) (h₂pos : r₂ > 0) (h₂ : Metric.eball x r₂ ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}), HasFPowerSeriesAt g p x
Tactic: rcases EMetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x_1 : E |
      Membership.mem (γ := Set E) (Metric.eball 0 r) x_1 →
        Membership.mem (γ := Set E)
          {x_2 : E |
            (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y)))
              x_2}
          x_1}
    a
Tactic: filter_upwards [Metric.eball_mem_nhds (0 : E) hf.r_pos] using fun _ => hf.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        Membership.mem (γ := Set E) (Metric.eball 0 r) x_1 →
          Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y)))
                x_2}
            x_1}
      a
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have h₁ : ∀ (a : E),
  Membership.mem (γ := Set E) (Metric.eball 0 r) a →
    HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ a) (f (x + a))
Tactic: filter_upwards [Metric.eball_mem_nhds (0 : E) hf.r_pos] using fun _ => hf.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x_1 : E |
      x_1 ∈ Metric.eball x r →
        Membership.mem (γ := Set E)
          {x_2 : E |
            (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
              x_2}
          x_1}
    a
Tactic: filter_upwards [Metric.eball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        x_1 ∈ Metric.eball x r →
          Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
                x_2}
            x_1}
      a
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
have h₁ : ∀ a ∈ Metric.eball x r, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ a - x) (f a)
Tactic: filter_upwards [Metric.eball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x r
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x_1 : E |
      Membership.mem (γ := Set E)
          {x_2 : E |
            (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
              x_2}
          x_1 →
        Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z = 0) x} x_1}
    a
Tactic: filter_upwards [hf.eventually_hasSum_sub] with z hz using hz.unique hasSum_zero
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x r
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
                x_2}
            x_1 →
          Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z = 0) x} x_1}
      a
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0
have h₁ : ∀ (a : E), HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ a - x) (f a) → f a = 0
Tactic: filter_upwards [hf.eventually_hasSum_sub] with z hz using hz.unique hasSum_zero
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r
have mp : HasFPowerSeriesWithinOnBall f p univ x r → HasFPowerSeriesOnBall f p x r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
mp : HasFPowerSeriesWithinOnBall f p univ x r → HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r
have mpr : HasFPowerSeriesOnBall f p x r → HasFPowerSeriesWithinOnBall f p univ x r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p s x r
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
h : t ⊆ s
⊢ HasFPowerSeriesWithinAt f p t x
have obtain : ∀ (r : ℝ≥0∞) (hp : HasFPowerSeriesWithinOnBall f p s x r), HasFPowerSeriesWithinAt f p t x
Tactic: obtain ⟨r, hp⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p s x
have hf₁ : HasFPowerSeriesWithinAt f p univ x
Tactic: rw [← hasFPowerSeriesWithinAt_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
h : HasFPowerSeriesWithinAt f p s x
hst : s ∈ 𝓝[t] x
⊢ HasFPowerSeriesWithinAt f p t x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r), HasFPowerSeriesWithinAt f p t x
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x
have rcases : ∀ (r' : ℝ≥0∞) (r'_pos : r' > 0) (hr' : Metric.eball x r' ∩ t ⊆ s), HasFPowerSeriesWithinAt f p t x
Tactic: rcases EMetric.mem_nhdsWithin_iff.1 hst with ⟨r', r'_pos, hr'⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
⊢ HasFPowerSeriesWithinAt f p t x
have refine : HasFPowerSeriesWithinOnBall f p t x (min r r')
Tactic: refine ⟨min r r', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
⊢ HasFPowerSeriesWithinOnBall f p t x (min r r')
have Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
Tactic: have Z := hr.of_le (by simp [r'_pos, hr.r_pos]) (min_le_left r r')
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
⊢ HasFPowerSeriesWithinOnBall f p t x (min r r')
have refine : ∀ {y : E} (hy : x + y ∈ insert x t) (h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y),
  HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
Tactic: refine ⟨Z.r_le, Z.r_pos, fun {y} hy h'y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
hy : x + y ∈ insert x t
h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have apply : x + y ∈ insert x s
Tactic: apply Z.hasSum ?_ h'y
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
hy : x + y ∈ insert x t
h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y
⊢ x + y ∈ insert x s
have hy₁ : y = 0 ∨ x + y ∈ t
Tactic: simp only [mem_insert_iff, add_eq_left] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y
hy : y = 0 ∨ x + y ∈ t
⊢ x + y ∈ insert x s
have inl : ∀ (h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) 0), x + 0 ∈ insert x s
Tactic: rcases hy with rfl | hy
Cleared hypotheses: y, h'y, hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y
hy : y = 0 ∨ x + y ∈ t
inl : ∀ (h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) 0), x + 0 ∈ insert x s
⊢ x + y ∈ insert x s
have inr : ∀ (hy : x + y ∈ t), x + y ∈ insert x s
Tactic: rcases hy with rfl | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 (min r r')) y
hy : x + y ∈ t
⊢ x + y ∈ insert x s
have apply : x + y ∈ Metric.eball x r' ∩ t
Tactic: apply mem_insert_of_mem _ (hr' ?_)