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 : ∀ (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
⊢ a * (‖y‖ / (↑r' : ℝ)) ≤ a

Tactic:
have ya : a * (‖y‖ / ↑r') ≤ a :=
    mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.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
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_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
this : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)

Tactic:
this.trans ?_

Premises used: LE.le.trans
-- 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_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
this : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
refine : C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ))) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- 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_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
this : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
⊢ 0 < a

Tactic:
have : 0 < a := ha.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∞
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_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
this_2 : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
this : 0 < a
hd : 0 < 1 - a
⊢ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ))) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)

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∞
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_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
this_2 : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
this : 0 < a
⊢ 0 < 1 - a

Tactic:
apply_rules [sub_pos.2, ha.2]

Premises used: Iff.mpr, sub_pos, And.right
-- 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
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
suffices : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a)

Tactic:
suffices ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / r')) ^ n / (1 - a * (‖y‖ / r')) by
    refine this.trans ?_
    have : 0 < a := ha.1
    gcongr
    apply_rules [sub_pos.2, ha.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∞
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
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
apply :
  ∀ (n : ℕ),
    norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n / (1 - a * (‖y‖ / (↑r' : ℝ)))

Tactic:
apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum ys this)

Premises used: norm_sub_le_of_geometric_bound_of_hasSum, And.right, HasFPowerSeriesWithinOnBall.hasSum, LE.le.trans_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∞
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_1 : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
n : ℕ
⊢ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖

Tactic:
ContinuousMultilinearMap.le_opNorm _ _

Premises used: ContinuousMultilinearMap.le_opNorm
-- 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_1 : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
n : ℕ
⊢ ‖p n‖ * ∏ _i : Fin n, ‖y‖ = ‖p n‖ * (↑r' : ℝ) ^ n * (‖y‖ / (↑r' : ℝ)) ^ n

Tactic:
simp [field, div_pow]

Premises used: div_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 : ℝ≥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_1 : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
n : ℕ
hbc : ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
⊢ ‖p n‖ * (↑r' : ℝ) ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n

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

Tactic:
apply hp
-- 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_1 : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
n : ℕ
rw : C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n)
rw₁ rw₂ : C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n) ≤ C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n)
⊢ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
rw [mul_pow, mul_assoc]

Premises used: mul_assoc, 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
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_1 : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < (↑r' : ℝ)
hr'0 : 0 < (↑r' : ℝ)
this : Membership.mem (γ := Set E) (Metric.eball 0 r) y
ya : a * (‖y‖ / (↑r' : ℝ)) ≤ a
n : ℕ
fun : ‖p n‖ * ∏ _i : Fin n, ‖y‖ = ‖p n‖ * (↑r' : ℝ) ^ n * (‖y‖ / (↑r' : ℝ)) ^ n
fun₁ : ‖p n‖ * (↑r' : ℝ) ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n
fun₂ : C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
⊢ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n

Tactic:
calc
    ‖(p n) fun _ : Fin n => y‖
    _ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_opNorm _ _
    _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by simp [field, div_pow]
    _ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp
    _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]

Premises used: Norm.norm, HMul.hMul, ContinuousMultilinearMap.le_opNorm, HDiv.hDiv, Fin, DFunLike.coe, 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
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : (↑r' : ℝ≥0∞) < r
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_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
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : (↑r' : ℝ≥0∞) < r
hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (↑r' : ℝ≥0∞) < r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_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
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 * (‖y‖ / (↑r' : ℝ))) ^ 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
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,
        ∀ (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
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 :
      ∀ (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 ^ 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 ^ n

Tactic:
obtain ⟨a, ha, C, hC, 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
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
⊢ ∃ (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 ^ n

Tactic:
⟨a, ha, C, hC, fun y hy n ys => (hp y hy n ys).trans ?_⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- 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
refine :
  ∀ (y : E) (hy : Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y) (n : ℕ) (ys : x + y ∈ insert x s),
    C * (a * (‖y‖ / (↑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 ^ n

Tactic:
refine ⟨a, ha, C, hC, fun y hy n ys => (hp y hy n ys).trans ?_⟩
-- 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
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hy : Membership.mem (γ := Set E) {x : E | ‖x‖ < (↑r' : ℝ)} y) (n : ℕ) (ys : x + y ∈ insert x s), ‖y‖ < (↑r' : ℝ)
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
rwa [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 :
  ∀ (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
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
have yr' : ‖y‖ < r' := by rwa [ball_zero_eq] at 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 :
  ∀ (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' : ℝ)
⊢ 0 ≤ a

Tactic:
have := ha.1.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
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
hbc : a * (‖y‖ / (↑r' : ℝ)) ≤ a
⊢ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n ≤ C * a ^ n

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∞
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:
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