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∞
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
n : ℕ
this : 0 < a
hbc :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 2)) ↦ E) F) (p (n + 2)) ≤
    C * a ^ (n + 2) / (↑r' : ℝ) ^ (n + 2)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 2)) ↦ E) F) (p (n + 2)) *
        ‖y - (x, x)‖ ^ n *
      ((↑(n + 2) : ℝ) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) ≤
    C * a ^ (n + 2) / (↑r' : ℝ) ^ (n + 2) * (↑r' : ℝ) ^ n * ((↑(n + 2) : ℝ) * ‖y - (x, x)‖ * ‖y.1 - y.2‖)
have hbc₁ : ‖y - (x, x)‖ ≤ (↑r' : ℝ)
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
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
⊢ ‖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
have hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
Tactic: have hAB : ∀ n, ‖A (n + 2)‖ ≤ B n := fun n =>
      calc
        ‖A (n + 2)‖ ≤ ‖p (n + 2)‖ * ↑(n + 2) * ‖y - (x, x)‖ ^ (n + 1) * ‖y.1 - y.2‖ := by
          simpa only [Fintype.card_fin, pi_norm_const, Prod.norm_def, Pi.sub_def,
            Prod.fst_sub, Prod.snd_sub, sub_sub_sub_cancel_right] using
            (p <| n + 2).norm_image_sub_le (fun _ => y.1 - x) fun _ => y.2 - x
        _ = ‖p (n + 2)‖ * ‖y - (x, x)‖ ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) := by
          rw [pow_succ ‖y - (x, x)‖]
          ring
        _ ≤ C * a ^ (n + 2) / r' ^ (n + 2)
            * r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) := by
          have : 0 < a := ha.1
          gcongr
          · apply hp
          · apply hy'.le
        _ = B n := by
          simp [field, B, pow_succ]
-- 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
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ HasSum B (L y)
have h : HasSum (fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * a ^ i) (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
Tactic: apply HasSum.mul_left
-- 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
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ HasSum (fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * a ^ i) (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
have h : HasSum (fun (i : ℕ) ↦ (↑i : ℝ) * a ^ i + 2 * a ^ i) (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
Tactic: simp only [add_mul]
-- 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∞
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ HasSum (fun (i : ℕ) ↦ (↑i : ℝ) * a ^ i + 2 * a ^ i) (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
have this : ‖a‖ < 1
Tactic: have : ‖a‖ < 1 := by simp only [Real.norm_eq_abs, abs_of_pos ha.1, ha.2]
-- 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∞
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 - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
hA :
  HasSum (fun (n : ℕ) ↦ A (n + 2))
    (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))
B : ℕ → ℝ :=
  fun (n : ℕ) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ ‖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
have hBL : HasSum B (L y)
Tactic: have hBL : HasSum B (L y) := by
      apply HasSum.mul_left
      simp only [add_mul]
      have : ‖a‖ < 1 := by simp only [Real.norm_eq_abs, abs_of_pos ha.1, ha.2]
      rw [div_eq_mul_inv, div_eq_mul_inv]
      exact (hasSum_coe_mul_geometric_of_norm_lt_one this).add
          ((hasSum_geometric_of_norm_lt_one this).mul_left 2)
-- 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
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))
hL :
  ∀ 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
⊢ 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 inr : IsBigO (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)) L fun (y : E × E) ↦
  ‖y - (x, x)‖ * ‖y.1 - y.2‖
Tactic: suffices L =O[𝓟 (Metric.eball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))]
      fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ from
    .trans (.of_norm_eventuallyLE (eventually_principal.2 hL)) this
-- 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
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))
hL :
  ∀ 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
⊢ IsBigO (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)) L fun (y : E × E) ↦
    ‖y - (x, x)‖ * ‖y.1 - y.2‖
have inr : IsBigO (E := ℝ) (F := ℝ) (𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s))
  (fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a)) *
      (‖y - (x, x)‖ * ‖y.1 - y.2‖))
  fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
Tactic: simp_rw [L, mul_right_comm _ (_ * _)]
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) r'))
    (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 hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, hr
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s ∩ Metric.eball x r',
      ∀ z ∈ insert x s ∩ Metric.eball x r',
        ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
          C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
have this : 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: have := hf.isBigO_image_sub_image_sub_deriv_principal 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  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‖
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s ∩ Metric.eball x r',
      ∀ z ∈ insert x s ∩ Metric.eball x r',
        ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
          C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
have simp : ∀
  (this :
    ∃ (c : ℝ),
      ∀ (a b : E),
        edist a x < r' →
          edist b x < r' →
            a ∈ insert x s →
              b ∈ insert x s →
                ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                  c * (‖(a, b) - (x, x)‖ * ‖a - b‖)),
  ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)
Tactic: simp only [isBigO_principal, mem_inter_iff, Metric.mem_eball, Prod.edist_eq, max_lt_iff, mem_prod,
    norm_mul, Real.norm_eq_abs, abs_norm, and_imp, Prod.forall, mul_assoc] at this ⊢
Cleared hypotheses: this
-- 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
this :
  ∃ (c : ℝ),
    ∀ (a b : E),
      edist a x < r' →
        edist b x < r' →
          a ∈ insert x s →
            b ∈ insert x s →
              ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                c * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)
have rcases : ∀ (C : ℝ)
  (hC :
    ∀ (a b : E),
      edist a x < r' →
        edist b x < r' →
          a ∈ insert x s →
            b ∈ insert x s →
              ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                C * (‖(a, b) - (x, x)‖ * ‖a - b‖)),
  ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)
Tactic: rcases this with ⟨C, hC⟩
Cleared hypotheses: this
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ ∃ (C : ℝ),
    ∀ y ∈ Metric.eball x r',
      ∀ z ∈ Metric.eball x r',
        ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
          C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, 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
hf : HasFPowerSeriesWithinAt f p s x
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (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 rcases : ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s x r),
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (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 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
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (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 rcases : ∀ (r' : ℝ≥0) (r'0 : 0 < (↑r' : ℝ≥0∞)) (h : (↑r' : ℝ≥0∞) < r),
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (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 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
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 := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (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 refine : 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)
Tactic: refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_
-- 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
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)
have rw : 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ Metric.eball (x, x) (↑r' : ℝ≥0∞))
Tactic: rw [inter_comm]
-- 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
hf : HasFPowerSeriesAt f p x
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 (x, x))
    (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 hf₁ : HasFPowerSeriesWithinAt f p univ x
Tactic: rw [← hasFPowerSeriesWithinAt_univ] at hf
Cleared hypotheses: hf