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
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‖
⊢ 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 : ∀ (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‖
Tactic: rcases eq_zero_or_pos r' with (rfl | hr'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
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
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‖
have 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‖
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)
-- 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‖ * (↑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‖
have hp₁ : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
Tactic: simp only [← le_div_iff₀ (pow_pos (NNReal.coe_pos.2 hr'0) _)] at hp
Cleared hypotheses: hp
-- 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
⊢ 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
have 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
Tactic: ⟨hy', ys⟩
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
⊢ y ∈ Metric.eball x r ×ˢ Metric.eball x r
have rw : y ∈ Metric.eball (x, x) r
Tactic: rw [Metric.eball_prod_same]
-- 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 ∈ 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
have hy : 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'
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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)
⊢ 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))
have h : 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) =
  f y.1 - f y.2 -
    ∑ i ∈ Finset.range 2,
      HSub.hSub (α := F) (β := F) ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.1 - x : F)
        ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.2 - x : F)
Tactic: convert!
        (hasSum_nat_add_iff' 2).2
          ((hf.hasSum_sub ⟨ys.1, hy.1⟩).sub (hf.hasSum_sub ⟨ys.2, hy.2⟩)) using 1
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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)
⊢ 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) =
    f y.1 - f y.2 -
      ∑ i ∈ Finset.range 2,
        HSub.hSub (α := F) (β := F) ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.1 - x : F)
          ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.2 - x : F)
have h : 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) =
  f y.1 - f y.2 -
    (∑ x_1 ∈ Finset.range 1,
        HSub.hSub (α := F) (β := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.1 - x : F)
          ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.2 - x : F) +
      HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
Tactic: rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
        zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
        ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
        ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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)
h :
  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) =
    f y.1 - f y.2 -
      (∑ x_1 ∈ Finset.range 1,
          HSub.hSub (α := F) (β := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.1 - x : F)
            ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
⊢ 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) =
    f y.1 - f y.2 -
      ∑ i ∈ Finset.range 2,
        HSub.hSub (α := F) (β := F) ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.1 - x : F)
          ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.2 - x : F)
have h₁ : 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) =
  f y.1 - f y.2 -
    (HSub.hSub (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.1 - x : F)
        ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.2 - x : F) +
      HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
Tactic: rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
        zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
        ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
        ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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)
h :
  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) =
    f y.1 - f y.2 -
      (∑ x_1 ∈ Finset.range 1,
          HSub.hSub (α := F) (β := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.1 - x : F)
            ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₁ :
  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) =
    f y.1 - f y.2 -
      (HSub.hSub (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.1 - x : F)
          ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
⊢ 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) =
    f y.1 - f y.2 -
      ∑ i ∈ Finset.range 2,
        HSub.hSub (α := F) (β := F) ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.1 - x : F)
          ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.2 - x : F)
have h₂ : 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) =
  f y.1 - f y.2 -
    (HSub.hSub (β := F) (f x) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.2 - x : F) +
      HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
Tactic: rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
        zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
        ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
        ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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)
⊢ ‖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 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))
Tactic: have hA : HasSum (fun n => A (n + 2)) (f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) := by
      convert!
        (hasSum_nat_add_iff' 2).2
          ((hf.hasSum_sub ⟨ys.1, hy.1⟩).sub (hf.hasSum_sub ⟨ys.2, hy.2⟩)) using 1
      rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
        zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
        ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
        ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
-- 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 ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
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))
⊢ ‖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 hy'₁ : ‖y - (x, x)‖₊ < r'
Tactic: rw [Metric.mem_eball, edist_eq_enorm_sub, enorm_lt_coe] at hy'
Cleared hypotheses: hy', ys, hy, A, hA
-- 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)
n : ℕ
⊢ 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 this : 0 < a
Tactic: have : 0 < a := ha.1
-- 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
⊢ 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 : 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)
Tactic: gcongr