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_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)), ‖w‖ ≤ (↑r' : ℝ)
⊢ LE.le (α := ℝ)
    (∑ 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))
    (∑ 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)) *
        (↑r' : ℝ) ^ (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)
⊢ ‖w‖ ≤ (↑r' : ℝ)

Tactic:
simpa [← coe_nnnorm] using hw.le

Premises used: LT.lt.le, 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
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)
⊢ 0 ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
      (↑r' : ℝ) ^ (i + k)

Tactic:
positivity
-- 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'
apply :
  Summable (α := ℝ) fun (i : ℕ) ↦
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
      (↑r' : ℝ) ^ (i + k)
⊢ LE.le (α := ℝ)
    (∑ 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)) *
        (↑r' : ℝ) ^ (i + k))
    (∑' (i : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
        (↑r' : ℝ) ^ (i + k))

Tactic:
apply Summable.sum_le_tsum _ (fun i _hi ↦ by positivity)

Premises used: Summable.sum_le_tsum
-- 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'
⊢ Summable (α := ℝ) fun (i : ℕ) ↦
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + k)) ↦ E) F) (p (i + k)) *
      (↑r' : ℝ) ^ (i + k)

Tactic:
apply ((_root_.summable_nat_add_iff k).2 S)

Premises used: Iff.mpr, summable_nat_add_iff
-- 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'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4

Tactic:
have I (w : E) (hw : ‖w‖₊ < r') : ‖∑ i ∈ Ico k n, p i (fun _ ↦ w)‖ ≤ ε / 4 := calc
    ‖∑ i ∈ Ico k n, p i (fun _ ↦ w)‖
    _ = ‖∑ i ∈ range (n - k), p (i + k) (fun _ ↦ w)‖ := by
        rw [sum_Ico_eq_sum_range]
        congr with i
        rw [add_comm k]
    _ ≤ ∑ i ∈ range (n - k), ‖p (i + k) (fun _ ↦ w)‖ := norm_sum_le _ _
    _ ≤ ∑ i ∈ range (n - k), ‖p (i + k)‖ * ‖w‖ ^ (i + k) := by
        gcongr with i _hi; exact ((p (i + k)).le_opNorm _).trans_eq (by simp)
    _ ≤ ∑ i ∈ range (n - k), ‖p (i + k)‖ * ↑r' ^ (i + k) := by
        gcongr with i _hi; simpa [← coe_nnnorm] using hw.le
    _ ≤ ∑' i, ‖p (i + k)‖ * ↑r' ^ (i + k) := by
        apply Summable.sum_le_tsum _ (fun i _hi ↦ by positivity)
        apply ((_root_.summable_nat_add_iff k).2 S)
    _ ≤ ε / 4 := hk.le
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
⊢ ‖p.partialSum n z - p.partialSum n y‖ =
    ‖HSub.hSub (α := F) (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖

Tactic:
rfl

Premises used: FormalMultilinearSeries.partialSum, rfl
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
⊢ ‖HSub.hSub (α := F) (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖ =
    ‖HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
        HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖

Tactic:
simp [sum_range_add_sum_Ico _ hkn]

Premises used: Finset.sum_range_add_sum_Ico
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
e_a :
  HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
      HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) =
    (p.partialSum k z - p.partialSum k y +
        ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y
⊢ ‖HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
        HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖ =
    ‖(p.partialSum k z - p.partialSum k y +
          ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
        -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y‖

Tactic:
congr 1
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
e_a :
  HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
      HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) =
    (HSub.hSub (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) +
        ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y
⊢ HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
      HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) =
    (p.partialSum k z - p.partialSum k y +
        ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y

Tactic:
simp only [FormalMultilinearSeries.partialSum]

Premises used: FormalMultilinearSeries.partialSum
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
⊢ HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
      HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
        (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) =
    (HSub.hSub (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) +
        ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y

Tactic:
abel
-- 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
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
⊢ ‖(p.partialSum k z - p.partialSum k y + ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
        -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y‖ ≤
    ‖p.partialSum k z - p.partialSum k y‖ +
        norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      norm.{u_3} (E := F) (-∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)

Tactic:
norm_add₃_le

Premises used: norm_add₃_le