Theorem: HasFPowerSeriesOnBall.unshift (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
⊢ ∀ {y : 𝕜}, y ∈ EMetric.ball 0 r → HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))
Tactic:
intro y yr
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))
Tactic:
simp only [FormalMultilinearSeries.apply_eq_pow_smul_coeff, add_sub_cancel_left]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => y ^ n • (p.unshift' 0).coeff n) (y • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => y ^ n • (p.unshift' 0).coeff n) (y • f (c + y))
Tactic:
generalize hs : (fun n ↦ y ^ n • (p.unshift' 0).coeff n) = s
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
⊢ HasSum s (y • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
⊢ HasSum s (y • f (c + y))
Tactic:
have s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s := by
  simp only [← hs, p.unshift_coeff_zero, Finset.range_one, Finset.sum_singleton, smul_zero,
    add_zero]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum s (y • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum s (y • f (c + y))
Tactic:
rw [s0, ← hasSum_nat_add_iff, ← hs]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => (fun n => y ^ n • (p.unshift' 0).coeff n) (n + 1)) (y • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => (fun n => y ^ n • (p.unshift' 0).coeff n) (n + 1)) (y • f (c + y))
Tactic:
simp only [p.unshift_coeff_succ, pow_succ', ← smul_smul]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => y • y ^ n • p.coeff n) (y • f (c + y))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => y • y ^ n • p.coeff n) (y • f (c + y))
Tactic:
apply HasSum.const_smul
State after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))

State before:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Tactic:
have h := fp.hasSum yr
State after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => (p n) fun x => y) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))

State before:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => (p n) fun x => y) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Tactic:
simp only [FormalMultilinearSeries.apply_eq_pow_smul_coeff] at h
State after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => y ^ n • p.coeff n) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))

State before:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => y ^ n • p.coeff n) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Tactic:
exact h
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
⊢ y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
Tactic:
simp only [← hs, p.unshift_coeff_zero, Finset.range_one, Finset.sum_singleton, smul_zero,
  add_zero]
State after:
no goals