awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
have refine_2 : ∀ x ∈ s, ∑' (n : ι), f n x = g x
Tactic: apply hc.congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
⊢ ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s
have refine_1 : ∀ (a : Finset ι),
  Membership.mem (γ := Set (Finset ι))
    {x : Finset ι | (fun (n : Finset ι) ↦ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s) x}
    a
Tactic: filter_upwards with t r hr using
      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
refine_1 :
  ∀ (a : Finset ι),
    Membership.mem (γ := Set (Finset ι))
      {x : Finset ι |
        (fun (n : Finset ι) ↦ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s) x}
      a
⊢ ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s
have refine_1₁ : ∀ (a : Finset ι), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ a, f i x2) s
Tactic: filter_upwards with t r hr using
      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
refine_1 :
  ∀ (a : Finset ι),
    Membership.mem (γ := Set (Finset ι))
      {x : Finset ι |
        (fun (n : Finset ι) ↦ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s) x}
      a
refine_1₁ : ∀ (a : Finset ι), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ a, f i x2) s
⊢ ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s
have refine_1₂ : ∀ (t : Finset ι) (r : ℂ) (hr : r ∈ s),
  DifferentiableWithinAt.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ t, f i x2) s r
Tactic: filter_upwards with t r hr using
      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'
have obtain : ∀ (r' : ℝ) (h₁ : dist c z < r') (h₂ : r' < r), ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'
Tactic: obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have obtain : ∀ (r' : ℝ) (hr' : r' < r) (hr'₀ : 0 < r') (hzr' : z ∈ Metric.ball c r'),
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
Tactic: obtain ⟨r', hr', hr'₀, hzr'⟩ : ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r' := by
    obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
    exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : ℝ
hr' : r' < r
hr'₀ : 0 < r'
hzr' : z ∈ Metric.ball c r'
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have lift : ∀ (r' : NNReal) (hr' : (↑r' : ℝ) < r) (hr'₀ : 0 < (↑r' : ℝ)) (hzr' : z ∈ Metric.ball c (↑r' : ℝ)),
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
Tactic: lift r' to NNReal using hr'₀.le
Cleared hypotheses: r', hr', hr'₀, hzr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : (↑r' : ℝ) < r
hr'₀ : 0 < (↑r' : ℝ)
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
⊢ Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)
have rw : Membership.mem (γ := Set ℂ) (Metric.ball 0 (↑r' : ℝ)) (z - c)
Tactic: rw [Metric.eball_coe]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : (↑r' : ℝ) < r
hr'₀ : 0 < (↑r' : ℝ)
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have hz' : Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)
Tactic: have hz' : z - c ∈ Metric.eball 0 r' := by
    rw [Metric.eball_coe]
    simpa only [mem_ball_iff_norm, sub_zero] using hzr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : (↑r' : ℝ) < r
hr'₀ : 0 < (↑r' : ℝ)
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
hz' : Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have H : HasSum
  (fun (n : ℕ) ↦
    HSMul.hSMul (α := ℂ) (β := E) (↑n ! : ℂ)⁻¹
      ((iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c : E))
  (f (c + (z - c)))
Tactic: have H := (hf.mono <| Metric.closedBall_subset_ball hr').hasFPowerSeriesOnBall hr'₀
      |>.hasSum_iteratedFDeriv hz'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : (↑r' : ℝ) < r
hr'₀ : 0 < (↑r' : ℝ)
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
hz' : Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)
H :
  HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℂ) (β := E) (↑n ! : ℂ)⁻¹
        ((iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c : E))
    (f (c + (z - c)))
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have H₁ : HasSum
  (fun (n : ℕ) ↦
    HSMul.hSMul (α := ℂ) (β := E) (↑n ! : ℂ)⁻¹
      ((iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c : E))
  (f z)
Tactic: simp only [add_sub_cancel] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : (↑r' : ℝ) < r
hr'₀ : 0 < (↑r' : ℝ)
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
hz' : Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)
H :
  HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℂ) (β := E) (↑n ! : ℂ)⁻¹
        ((iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c : E))
    (f z)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have h : ∀ (n : ℕ),
  (z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c
Tactic: convert! H using 4 with n
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
have h : ∀ (n : ℕ),
  (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: convert! taylorSeries_eq_on_ball hf hz using 3 with n
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₃ : (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have obtain : ∀ (r' : ENNReal) (hzr' : edist c z < r') (hr' : r' < r),
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
Tactic: obtain ⟨r', hzr', hr'⟩ := exists_between (Metric.mem_eball'.mp hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : ENNReal
hzr' : edist c z < r'
hr' : r' < r
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have lift : ∀ (r' : NNReal) (hzr' : edist c z < (↑r' : ENNReal)) (hr' : (↑r' : ENNReal) < r),
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
Tactic: lift r' to NNReal using ne_top_of_lt hr'
Cleared hypotheses: r', hzr', hr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : edist c z < (↑r' : ENNReal)
hr' : (↑r' : ENNReal) < r
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have hzr'₁ : z ∈ Metric.ball c (↑r' : ℝ)
Tactic: rw [← Metric.mem_eball', Metric.eball_coe] at hzr'
Cleared hypotheses: hzr', hr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
hr' : (↑r' : ENNReal) < r
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)
have refine : DifferentiableOn ℂ f (Metric.ball c (↑r' : ℝ))
Tactic: refine hasSum_taylorSeries_on_ball ?_ hzr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : z ∈ Metric.ball c (↑r' : ℝ)
hr' : (↑r' : ENNReal) < r
⊢ DifferentiableOn ℂ f (Metric.ball c (↑r' : ℝ))
have rw : DifferentiableOn ℂ f (Metric.eball c (↑r' : ENNReal))
Tactic: rw [← Metric.eball_coe]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
have h : ∀ (n : ℕ),
  (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: convert! taylorSeries_eq_on_eball hf hz using 3 with n
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₃ : (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
have h : ∀ (n : ℕ),
  (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: convert! taylorSeries_eq_of_entire hf c z using 3 with n
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.TaylorSeries (goal)
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
h :
  (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
h₁ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * (z - c) ^ n • iteratedDeriv n f c
h₂ : (↑n ! : ℂ)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
⊢ (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
    HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
have h₃ : (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n ! : ℂ)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Tactic: rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have have : ∀ (this : NormedSpace ℝ E), TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
Tactic: have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this : NormedSpace ℝ E
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have this₁ : IsScalarTower ℝ 𝕜 E
Tactic: have : IsScalarTower ℝ 𝕜 E := Real.isScalarTower
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have refine_1 : ∀ (x : E),
  Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
Tactic: refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
refine_1 :
  ∀ (x : E),
    Membership.mem (γ := Set E) (Metric.closedBall 0 1)
      (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have refine_2 : Eq (α := C((↑(Metric.closedBall 0 1) : Type w), (↑(Metric.closedBall 0 1) : Type w)))
  (ContinuousMap.comp
    { toFun := codRestrict (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g) (Metric.closedBall 0 1) sorry,
      continuous_toFun := sorry : C(E, (↑(Metric.closedBall 0 1) : Type w)) }
    { toFun := Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
      continuous_toFun := sorry })
  (ContinuousMap.id (↑(Metric.closedBall 0 1) : Type w))
Tactic: refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_