awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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' : ℝ
h₁ : dist c z < r'
h₂ : r' < r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Metric.pos_of_mem_ball, Metric.mem_ball'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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' : ℝ
h₁ : dist c z < r'
h₂ : r' < r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
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)
⊢ 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₁⟩
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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'
⊢ 0 ≤ r'

Tactic:
hr'₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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'
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)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)

Tactic:
lift r' to NNReal using hr'₀.le

Premises used: LT.lt.le, NNReal
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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' : ℝ)
rw : Membership.mem (γ := Set ℂ) (Metric.ball 0 (↑r' : ℝ)) (z - c)
⊢ Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r' : ENNReal)) (z - c)

Tactic:
rw [Metric.eball_coe]

Premises used: Metric.eball_coe
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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.ball 0 (↑r' : ℝ)) (z - c)

Tactic:
simpa only [mem_ball_iff_norm, sub_zero] using hzr'

Premises used: sub_zero, mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)

Tactic:
have hz' : z - c ∈ Metric.eball 0 r' := by
    rw [Metric.eball_coe]
    simpa only [mem_ball_iff_norm, sub_zero] using hzr'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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 (α := ℂ) (β := 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'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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 (α := ℂ) (β := 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

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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 (α := ℂ) (β := E) (↑n ! : ℂ)⁻¹
        ((iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c : E))
    (f z)

Tactic:
H
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)
h :
  ∀ (n : ℕ),
    (z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)

Tactic:
convert! H using 4 with n
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)
n : ℕ
⊢ (z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ z - c

Tactic:
simpa only [iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, mul_one, Finset.prod_const,
    Finset.card_fin]
    using ((iteratedFDeriv ℂ n f c).map_smul_univ (fun _ ↦ z - c) (fun _ ↦ 1)).symm

Premises used: ContinuousMultilinearMap.map_smul_univ, HSub.hSub, Finset.prod_const, Finset.card_fin, iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, iteratedFDeriv, mul_one, Complex, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
(hasSum_taylorSeries_on_ball hf hz).tsum_eq

Premises used: Complex.hasSum_taylorSeries_on_ball, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
taylorSeries_eq_on_ball hf hz

Premises used: Complex.taylorSeries_eq_on_ball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h :
  ∀ (n : ℕ),
    (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
      HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_on_ball hf hz using 3 with n

Premises used: Complex.taylorSeries_eq_on_ball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)
h₃ 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)

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, mul_right_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
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)
⊢ 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)

Premises used: exists_between, Iff.mp, Metric.mem_eball'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
⊢ r' ≠ ⊤

Tactic:
ne_top_of_lt hr'

Premises used: ne_top_of_lt
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
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)
⊢ 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'

Premises used: NNReal, ne_top_of_lt
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
⊢ z ∈ Metric.ball c (↑r' : ℝ)

Tactic:
rw [← Metric.mem_eball', Metric.eball_coe] at hzr'

Premises used: Metric.eball_coe, Metric.mem_eball'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
hzr'₁ : z ∈ Metric.ball c (↑r' : ℝ)
⊢ (↑r' : ENNReal) < r

Tactic:
rw [← Metric.mem_eball', Metric.eball_coe] at hzr'

Premises used: Metric.eball_coe, Metric.mem_eball'
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)

Tactic:
hasSum_taylorSeries_on_ball ?_ hzr'

Premises used: Complex.hasSum_taylorSeries_on_ball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
refine : DifferentiableOn ℂ f (Metric.ball c (↑r' : ℝ))
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)

Tactic:
refine hasSum_taylorSeries_on_ball ?_ hzr'

Premises used: Complex.hasSum_taylorSeries_on_ball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
rw : DifferentiableOn ℂ f (Metric.eball c (↑r' : ENNReal))
⊢ DifferentiableOn ℂ f (Metric.ball c (↑r' : ℝ))

Tactic:
rw [← Metric.eball_coe]

Premises used: Metric.eball_coe
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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.eball c (↑r' : ENNReal))

Tactic:
hf.mono <| Metric.eball_subset_eball hr'.le

Premises used: Metric.eball_subset_eball, LT.lt.le, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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.eball c (↑r' : ENNReal))

Tactic:
exact hf.mono <| Metric.eball_subset_eball hr'.le

Premises used: Metric.eball_subset_eball, LT.lt.le, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
(hasSum_taylorSeries_on_eball hf hz).tsum_eq

Premises used: HasSum.tsum_eq, Complex.hasSum_taylorSeries_on_eball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
taylorSeries_eq_on_eball hf hz

Premises used: Complex.taylorSeries_eq_on_eball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
h :
  ∀ (n : ℕ),
    (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
      HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_on_eball hf hz using 3 with n

Premises used: Complex.taylorSeries_eq_on_eball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)
h₃ 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)

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, mul_right_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
hf : Differentiable ℂ f
c z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)) (f z)

Tactic:
hasSum_taylorSeries_on_eball hf.differentiableOn <| Metric.mem_eball.mpr <|
    edist_lt_top ..

Premises used: Iff.mpr, edist_lt_top, Differentiable.differentiableOn, Metric.mem_eball, Complex.hasSum_taylorSeries_on_eball
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
hf : Differentiable ℂ f
c z : ℂ
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
(hasSum_taylorSeries_of_entire hf c z).tsum_eq

Premises used: Complex.hasSum_taylorSeries_of_entire, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
⊢ ∑' (n : ℕ), HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c) = f z

Tactic:
taylorSeries_eq_of_entire hf c z

Premises used: Complex.taylorSeries_eq_of_entire
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
h :
  ∀ (n : ℕ),
    (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n =
      HSMul.hSMul (α := ℂ) (↑n ! : ℂ)⁻¹ ((z - c) ^ n • iteratedDeriv n f c)
⊢ ∑' (n : ℕ), (↑n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_of_entire hf c z using 3 with n

Premises used: Complex.taylorSeries_eq_of_entire
-- Module: Mathlib.Analysis.Complex.TaylorSeries
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)
h₃ 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)

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, mul_right_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : CompleteSpace 𝕜
inst_9 : TietzeExtension 𝕜
⊢ TietzeExtension E

Tactic:
Module.Basis.ofVectorSpace 𝕜 E |>.equivFun.toContinuousLinearEquiv.toHomeomorph |> .of_homeo

Premises used: Module.Basis.ofVectorSpace, ContinuousLinearEquiv.toHomeomorph, LinearEquiv.toContinuousLinearEquiv, TietzeExtension.of_homeo, Module.Basis.equivFun
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
⊢ TietzeExtension ℂ

Tactic:
TietzeExtension.of_tvs ℝ

Premises used: Real, TietzeExtension.of_tvs
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ TietzeExtension 𝕜

Tactic:
TietzeExtension.of_tvs ℝ

Premises used: Real, TietzeExtension.of_tvs
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
inst_7 : FiniteDimensional 𝕜 E
⊢ TietzeExtension E

Tactic:
TietzeExtension.of_tvs 𝕜

Premises used: TietzeExtension.of_tvs
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ TietzeExtension.{u, w} (↑(Metric.ball 0 1) : Type w)

Tactic:
have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  .of_homeo Homeomorph.unitBall.symm

Premises used: Real, Homeomorph.unitBall, Homeomorph.symm, NormedSpace.restrictScalars, TietzeExtension.of_homeo
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
have : ∀ (this : NormedSpace ℝ E), TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)

Tactic:
have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this : NormedSpace ℝ E
⊢ IsScalarTower ℝ 𝕜 E

Tactic:
have : IsScalarTower ℝ 𝕜 E := Real.isScalarTower
-- Module: Mathlib.Analysis.Complex.Tietze
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)
⊢ Continuous.{w, w} (X := (↑(Metric.closedBall 0 1) : Type w))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x))

Tactic:
fun_prop