awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
this : ContinuousAt.{u_2, u_3} (Y := F) (fun (z : E) ↦ p.partialSum k z) y
⊢ ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4

Tactic:
exact tendsto_snd (Metric.tendsto_nhds.1 this.tendsto (ε / 4) (by linarith))

Premises used: Metric.tendsto_nhds, HDiv.hDiv, ContinuousAt.tendsto, Iff.mp, OfNat.ofNat, Filter.tendsto_snd
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
⊢ ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4

Tactic:
have A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y,
      dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4 := by
    have : ContinuousAt (fun z ↦ p.partialSum k z) y := (p.partialSum_continuous k).continuousAt
    exact tendsto_snd (Metric.tendsto_nhds.1 this.tendsto (ε / 4) (by linarith))
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
suffices : ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r'
⊢ ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'

Tactic:
suffices ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r' from tendsto_snd this
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
⊢ Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y

Tactic:
simpa using yr'_2
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
⊢ Metric.ball 0 (↑r' : ℝ) ∈ 𝓝 y

Tactic:
have : Metric.ball 0 r' ∈ 𝓝 y := Metric.isOpen_ball.mem_nhds (by simpa using yr'_2)
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
this : Metric.ball 0 (↑r' : ℝ) ∈ 𝓝 y
a : E
ha : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) a
⊢ ‖a‖₊ < r'

Tactic:
simpa [← coe_nnnorm] using ha

Premises used: coe_nnnorm
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
this : Metric.ball 0 (↑r' : ℝ) ∈ 𝓝 y
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) x →
          Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ ‖z‖₊ < r') x} x}
      a
h₁ h₂ : ∀ (a : E) (ha : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) a), ‖a‖₊ < r'
⊢ ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r'

Tactic:
filter_upwards [this] with a ha using by simpa [← coe_nnnorm] using ha
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
⊢ ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'

Tactic:
have B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r' := by
    suffices ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r' from tendsto_snd this
    have : Metric.ball 0 r' ∈ 𝓝 y := Metric.isOpen_ball.mem_nhds (by simpa using yr'_2)
    filter_upwards [this] with a ha using by simpa [← coe_nnnorm] using ha
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
⊢ ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1

Tactic:
have C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1 := tendsto_fst (Ici_mem_atTop _)
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
h :
  ∀ (a : ℕ × E),
    dist (p.partialSum k a.2) (p.partialSum k y) < ε / 4 →
      ‖a.2‖₊ < r' → k ≤ a.1 → dist (p.partialSum a.1 a.2 - p.partialSum a.1 y) 0 < ε
⊢ ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε

Tactic:
filter_upwards [A, B, C]
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
hz : dist (p.partialSum k (n, z).2) (p.partialSum k y) < ε / 4
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
h : ∀ (hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4), ‖p.partialSum n z - p.partialSum n y‖ < ε
⊢ dist (p.partialSum (n, z).1 (n, z).2 - p.partialSum (n, z).1 y) 0 < ε

Tactic:
simp only [dist_eq_norm, sub_zero] at hz ⊢

Premises used: dist_eq_norm, sub_zero
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
rw :
  norm.{u_3} (E := F)
      (∑ k_1 ∈ Finset.range (n - k), (p (k + k_1) : (a : (i : Fin (k + k_1)) → E) → F) fun (x : Fin (k + k_1)) ↦ w) =
    norm.{u_3} (E := F)
      (∑ i ∈ Finset.range (n - k), (p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w)
⊢ norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) =
    norm.{u_3} (E := F)
      (∑ i ∈ Finset.range (n - k), (p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w)

Tactic:
rw [sum_Ico_eq_sum_range]

Premises used: Finset.sum_Ico_eq_sum_range
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
e_a :
  ∀ (i : ℕ),
    Eq.{u_3 + 1} (α := F) ((p (k + i) : (a : (i : Fin (k + i)) → E) → F) fun (x : Fin (k + i)) ↦ w : F)
      ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F)
⊢ norm.{u_3} (E := F)
      (∑ k_1 ∈ Finset.range (n - k), (p (k + k_1) : (a : (i : Fin (k + k_1)) → E) → F) fun (x : Fin (k + k_1)) ↦ w) =
    norm.{u_3} (E := F)
      (∑ i ∈ Finset.range (n - k), (p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
e_a e_a₁ :
  Eq.{u_3 + 1} (α := F) ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F)
    ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F)
⊢ Eq.{u_3 + 1} (α := F) ((p (k + i) : (a : (i : Fin (k + i)) → E) → F) fun (x : Fin (k + i)) ↦ w : F)
    ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F)

Tactic:
rw [add_comm k]

Premises used: add_comm
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
h :
  ∀ (i : ℕ) (_hi : i ∈ Finset.range (n - k)),
    norm.{u_3} (E := F) ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F) ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
        ‖w‖ ^ (i + k)
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (n - k),
      norm.{u_3} (E := F) ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F))
    (∑ i ∈ Finset.range (n - k),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
        ‖w‖ ^ (i + k))

Tactic:
gcongr with i _hi
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
_hi : i ∈ Finset.range (n - k)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
      ∏ i : Fin (i + k), ‖w‖ =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) * ‖w‖ ^ (i + k)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Basic
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
_hi : i ∈ Finset.range (n - k)
⊢ norm.{u_3} (E := F) ((p (i + k) : (a : (i : Fin (i + k)) → E) → F) fun (x : Fin (i + k)) ↦ w : F) ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) * ‖w‖ ^ (i + k)

Tactic:
exact ((p (i + k)).le_opNorm _).trans_eq (by simp)

Premises used: LE.le.trans_eq, ContinuousMultilinearMap.le_opNorm, HAdd.hAdd