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∞
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 :
  ∀ (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
y : E
hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
this : 0 ≤ a
⊢ a * (‖y‖ / (↑r' : ℝ)) ≤ a

Tactic:
exact mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.coe_nonneg)

Premises used: div_le_one_of_le₀, mul_le_of_le_one_right, LT.lt.le, And.left, NNReal.coe_nonneg
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : (↑r' : ℝ≥0∞) < r
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      ∃ C > 0,
        ∀ (y : E),
          Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
            ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Tactic:
simpa using hf.uniform_geometric_approx h

Premises used: HasFPowerSeriesWithinOnBall.uniform_geometric_approx
-- 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
hf : HasFPowerSeriesWithinAt f p s x
n : ℕ
rcases :
  ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s x r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
      (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
    (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
rcases hf with ⟨r, hf⟩
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
rcases :
  ∀ (r' : ℝ≥0) (r'0 : 0 < (↑r' : ℝ≥0∞)) (h : (↑r' : ℝ≥0∞) < r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
      (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
    (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp, HasFPowerSeriesWithinOnBall.r_pos
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
⊢ ∃ (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:
hf.uniform_geometric_approx' h

Premises used: HasFPowerSeriesWithinOnBall.uniform_geometric_approx'
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
obtain :
  ∀ (a C : ℝ)
    (hp :
      ∀ (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),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
      (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
    (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
obtain ⟨a, -, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
      x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
    hf.uniform_geometric_approx' h

Premises used: HasFPowerSeriesWithinOnBall.uniform_geometric_approx', Metric.ball, OfNat.ofNat, NNReal.toReal, 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
    (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Asymptotics.isBigO_iff, HDiv.hDiv, HPow.hPow, Exists.intro, NNReal.toReal
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
refine :
  ∀ᶠ (x_1 : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0,
    ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / (↑r' : ℝ)) ^ n * ‖‖x_1‖ ^ n‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0)
    (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
refine isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Asymptotics.isBigO_iff, HDiv.hDiv, HPow.hPow, Exists.intro, NNReal.toReal
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
⊢ 0 < (↑r' : ℝ)

Tactic:
replace r'0 : 0 < (r' : ℝ) := mod_cast r'0
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
r'0 : 0 < (↑r' : ℝ)
h₁ :
  ∀ (y : E) (hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) y),
    ‖f (x + y) - p.partialSum n y‖ ≤ C * (a / (↑r' : ℝ)) ^ n * ‖‖y‖ ^ n‖
⊢ ∀ᶠ (x_1 : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] 0,
    ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / (↑r' : ℝ)) ^ n * ‖‖x_1‖ ^ n‖

Tactic:
filter_upwards [inter_mem_nhdsWithin _ (Metric.ball_mem_nhds (0 : E) r'0)] with y hy

Premises used: inter_mem_nhdsWithin, Metric.ball_mem_nhds, 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
r'0 : 0 < (↑r' : ℝ)
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) y
⊢ x + y ∈ insert x s

Tactic:
simpa using hy.1

Premises used: And.left
-- 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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
h : (↑r' : ℝ≥0∞) < r
a C : ℝ
hp :
  ∀ (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
r'0 : 0 < (↑r' : ℝ)
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) y
⊢ ‖f (x + y) - p.partialSum n y‖ ≤ C * (a / (↑r' : ℝ)) ^ n * ‖‖y‖ ^ n‖

Tactic:
simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div, div_pow]
    using hp y hy.2 n (by simpa using hy.1)

Premises used: mul_assoc, mul_div_assoc, div_mul_eq_mul_div, And.right, div_pow, mul_pow
-- 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
hf : HasFPowerSeriesAt f p x
n : ℕ
rw :
  ∀ (hf : HasFPowerSeriesWithinAt f p univ x) (n : ℕ),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Premises used: hasFPowerSeriesWithinAt_univ
-- 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
hf : HasFPowerSeriesWithinAt f p univ x
n : ℕ
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ f (x + y) - p.partialSum n y) fun (y : E) ↦ ‖y‖ ^ n

Tactic:
simpa using hf.isBigO_sub_partialSum_pow n

Premises used: HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
⊢ r' ≠ ∞

Tactic:
ne_top_of_lt hr

Premises used: ne_top_of_lt
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
lift :
  ∀ (r' : ℝ≥0) (hr : (↑r' : ℝ≥0∞) < r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
lift r' to ℝ≥0 using ne_top_of_lt hr

Premises used: ne_top_of_lt
-- 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
inl :
  ∀ (hr : (↑0 : ℝ≥0∞) < r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑0 : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
inr :
  ∀ (hr'0 : 0 < r'),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rcases eq_zero_or_pos r' with (rfl | hr'0)

Premises used: eq_zero_or_pos, 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : (↑0 : ℝ≥0∞) < r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑0 : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simp only [ENNReal.coe_zero, Metric.eball_zero, empty_inter, principal_empty, isBigO_bot]

Premises used: Metric.eball_zero, Set.empty_inter, ENNReal.coe_zero, Asymptotics.isBigO_bot, Filter.principal_empty
-- 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 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 (hr.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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
inr :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : 0 < C)
    (hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
obtain ⟨a, ha, C, hC : 0 < C, 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 (hr.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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
⊢ ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n

Tactic:
simp only [← le_div_iff₀ (pow_pos (NNReal.coe_pos.2 hr'0) _)] at hp

Premises used: Iff.mpr, pow_pos, NNReal.coe_pos, le_div_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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
this :
  ∀ (hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)) (ys : y ∈ insert x s ×ˢ insert x s),
    ‖HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F)‖ ≤ L y
⊢ y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s →
    ‖HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F)‖ ≤ L y

Tactic:
⟨hy', 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
rw : y ∈ Metric.eball (x, x) r
⊢ y ∈ Metric.eball x r ×ˢ Metric.eball x r

Tactic:
rw [Metric.eball_prod_same]

Premises used: Metric.eball_prod_same
-- 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
⊢ y ∈ Metric.eball (x, x) r

Tactic:
Metric.eball_subset_eball hr.le hy'

Premises used: Metric.eball_subset_eball, LT.lt.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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
⊢ y ∈ Metric.eball (x, x) r

Tactic:
exact Metric.eball_subset_eball hr.le hy'

Premises used: Metric.eball_subset_eball, LT.lt.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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
⊢ y ∈ Metric.eball x r ×ˢ Metric.eball x r

Tactic:
have hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r := by
      rw [Metric.eball_prod_same]
      exact Metric.eball_subset_eball hr.le hy'