-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m) s)
    (ha : ∀ k < n, a k = 0) : ∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < 0, a k = 0
⊢ ∃ t, z ^ 0 • t = s ∧ HasSum (fun m => z ^ m • a (m + 0)) t

Tactic:
simpa

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < 0, a k = 0
⊢ ∃ t, z ^ 0 • t = s ∧ HasSum (fun m => z ^ m • a (m + 0)) t

case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ (m + n) • a (m + n)) s

Tactic:
simpa [h1] using (hasSum_nat_add_iff' n).mpr hs

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Tactic:
refine ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], ?_⟩

Result:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Tactic:
have h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0 :=
  Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]

Result:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m => z ^ m • a m) 0

Tactic:
simpa [ha 0 hn, h] using hasSum_at_zero a

Result:
no goals

Proof state:
case h.e'_5
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (fun m => z ^ m • a (m + n)) = fun i => z⁻¹ ^ n • z ^ (i + n) • a (i + n)

Tactic:
field_simp [pow_add, smul_smul]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Tactic:
have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by
  simpa [h1] using (hasSum_nat_add_iff' n).mpr hs

Result:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Tactic:
convert h2.const_smul (z⁻¹ ^ n) using 1

Result:
case h.e'_5
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (fun m => z ^ m • a (m + n)) = fun i => z⁻¹ ^ n • z ^ (i + n) • a (i + n)

case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (z ^ n)⁻¹ • s = z⁻¹ ^ n • s

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Tactic:
by_cases h : z = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Tactic:
have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t