awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n
have hbc : ‖p n‖ * (↑r' : ℝ) ^ n ≤ C * a ^ n
Tactic: gcongr ?_ * _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 : ℕ
⊢ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
have rw : C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n)
Tactic: rw [mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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)
⊢ C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
have rw₁ : C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n) ≤ C * (a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n)
Tactic: rw [mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
have fun : ‖p n‖ * ∏ _i : Fin n, ‖y‖ = ‖p n‖ * (↑r' : ℝ) ^ n * (‖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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
have fun₁ : ‖p n‖ * (↑r' : ℝ) ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ C * a ^ n * (‖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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) ≤ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n
have fun₂ : C * a ^ n * (‖y‖ / (↑r' : ℝ)) ^ n ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∃ (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
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 ^ n
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
have 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
Tactic: refine ⟨a, ha, C, hC, fun y hy n ys => (hp y hy n ys).trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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' : ℝ)
have rwa : ∀ (hy : Membership.mem (γ := Set E) {x : E | ‖x‖ < (↑r' : ℝ)} y) (n : ℕ) (ys : x + y ∈ insert x s), ‖y‖ < (↑r' : ℝ)
Tactic: rwa [ball_zero_eq] at hy
Cleared hypotheses: hy, n, ys
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n ≤ C * a ^ n
have yr' : ‖y‖ < (↑r' : ℝ)
Tactic: have yr' : ‖y‖ < r' := by rwa [ball_zero_eq] at hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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' : ℝ)
⊢ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n ≤ C * a ^ n
have this : 0 ≤ a
Tactic: have := ha.1.le
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ C * (a * (‖y‖ / (↑r' : ℝ))) ^ n ≤ C * a ^ n
have hbc : a * (‖y‖ / (↑r' : ℝ)) ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∃ (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
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rcases hf with ⟨r, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ 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
have 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
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
have 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‖
Tactic: refine isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∀ᶠ (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‖
have r'0₁ : 0 < (↑r' : ℝ)
Tactic: replace r'0 : 0 < (r' : ℝ) := mod_cast r'0
Cleared hypotheses: r'0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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' : ℝ)
⊢ ∀ᶠ (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‖
have 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‖
Tactic: filter_upwards [inter_mem_nhdsWithin _ (Metric.ball_mem_nhds (0 : E) r'0)] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rw [← hasFPowerSeriesWithinAt_univ] at hf
Cleared hypotheses: hf, n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ 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‖
have 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‖
Tactic: lift r' to ℝ≥0 using ne_top_of_lt hr
Cleared hypotheses: r', hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ 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‖
have 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‖
Tactic: rcases eq_zero_or_pos r' with (rfl | hr'0)
Cleared hypotheses: r', hr