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
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
h₁ : norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) ≤ ε / 4
h₂ : norm.{u_3} (E := F) (-∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) ≤ ε / 4
⊢ ‖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) ≤
    ε / 4 + ε / 4 + ε / 4

Tactic:
gcongr
-- 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
⊢ norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) ≤ ε / 4

Tactic:
I _ h'z
-- 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
⊢ norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) ≤ ε / 4

Tactic:
exact I _ h'z
-- 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
h₂ : norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) ≤ ε / 4
⊢ norm.{u_3} (E := F) (-∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) ≤ ε / 4

Tactic:
simp only [norm_neg]

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

Tactic:
I _ yr'
-- 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
⊢ norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) ≤ ε / 4

Tactic:
exact I _ yr'
-- 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
linarith : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₁ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε ≤ ε / 4 + ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₈ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : ε ≤ ε / 4 + ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₁₀ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₁₁ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₂ : ε ≤ ε / 4 + ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₁₃ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 0 - ε + (4 * ε - (1 * ε + 1 * ε + 1 * ε)) = 0
⊢ ε / 4 + ε / 4 + ε / 4 < ε

Tactic:
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
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesOnBall f p x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Membership.mem (γ := Set E) (insert x univ) (x + y)

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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n

Tactic:
p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le)

Premises used: HasFPowerSeriesWithinOnBall.r_le, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, LT.lt.trans_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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
obtain :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
    (hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n),
    ∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        ∃ C > 0,
          ∀ (y : E),
            Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
              ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      ∃ C > 0,
        ∀ (y : E),
          Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
            ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
obtain ⟨a, ha, C, hC, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n, ‖p n‖ * (r' : ℝ) ^ n ≤ C * a ^ n :=
    p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le)

Premises used: HasFPowerSeriesWithinOnBall.r_le, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, LT.lt.trans_le, OfNat.ofNat, Set.Ioo
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      ∃ C > 0,
        ∀ (y : E),
          Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
            ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n ys => ?_⟩

Premises used: Iff.mpr, sub_pos, HSub.hSub, HDiv.hDiv, And.right, And.intro, Exists.intro, div_pos, OfNat.ofNat
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
refine :
  ∀ (y : E) (hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y) (n : ℕ) (ys : x + y ∈ insert x s),
    ‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / (↑r' : ℝ))) ^ n
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      ∃ C > 0,
        ∀ (y : E),
          Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
            ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n ys => ?_⟩
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
rw : ∀ (hy : Membership.mem (γ := Set E) {x : E | ‖x‖ < (↑r' : ℝ)} y) (n : ℕ) (ys : x + y ∈ insert x s), ‖y‖ < (↑r' : ℝ)
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
rw [ball_zero_eq] at hy

Premises used: ball_zero_eq
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) {x : E | ‖x‖ < (↑r' : ℝ)} y
n : ℕ
ys : x + y ∈ insert x s
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
hy

Premises used: Set.Mem
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) {x : E | ‖x‖ < (↑r' : ℝ)} y
n : ℕ
ys : x + y ∈ insert x s
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
exact hy
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
have yr' : ‖y‖ < r' := by
    rw [ball_zero_eq] at hy
    exact hy
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
⊢ 0 < (↑r' : ℝ)

Tactic:
have hr'0 : 0 < (r' : ℝ) := (norm_nonneg _).trans_lt yr'
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) y

Tactic:
mem_eball_zero_iff.2 (lt_trans ?_ h)

Premises used: Iff.mpr, Set.Mem, lt_trans, mem_eball_zero_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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
refine : ‖y‖ₑ < (↑r' : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) y

Tactic:
refine mem_eball_zero_iff.2 (lt_trans ?_ h)

Premises used: Iff.mpr, lt_trans, mem_eball_zero_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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
⊢ ‖y‖ₑ < (↑r' : ℝ≥0∞)

Tactic:
simpa [enorm] using yr'

Premises used: ENorm.enorm
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) y

Tactic:
have : y ∈ Metric.eball (0 : E) r := by
    refine mem_eball_zero_iff.2 (lt_trans ?_ h)
    simpa [enorm] using yr'
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
rw : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)
⊢ ‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
rw [norm_sub_rev, ← mul_div_right_comm]

Premises used: mul_div_right_comm, norm_sub_rev