Theorem: FormalMultilinearSeries.unshiftIter_coeff (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
p : FormalMultilinearSeries 𝕜 𝕜 E
n i : ℕ
⊢ (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n)
Tactic:
revert i
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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ∀ (i : ℕ), (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n)

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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ∀ (i : ℕ), (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n)
Tactic:
induction' n with n h
State after:
case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ ∀ (i : ℕ), (p.unshiftIter 0).coeff i = if i < 0 then 0 else p.coeff (i - 0)

case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (p.unshiftIter (n + 1)).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ ∀ (i : ℕ), (p.unshiftIter 0).coeff i = if i < 0 then 0 else p.coeff (i - 0)
Tactic:
simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_zero, id_eq, not_lt_zero',
  tsub_zero, if_false, eq_self_iff_true, forall_const, Nat.zero_eq]
State after:
no goals

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (p.unshiftIter (n + 1)).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
simp_rw [FormalMultilinearSeries.unshiftIter] at h
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (p.unshiftIter (n + 1)).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (p.unshiftIter (n + 1)).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_succ', Function.comp]
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (((fun p => p.unshift' 0)^[n] p).unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (((fun p => p.unshift' 0)^[n] p).unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
generalize hq : (fun p : FormalMultilinearSeries 𝕜 𝕜 E ↦ p.unshift' 0)^[n] p = q
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : (fun p => p.unshift' 0)^[n] p = q
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : ∀ (i : ℕ), ((fun p => p.unshift' 0)^[n] p).coeff i = if i < n then 0 else p.coeff (i - n)
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : (fun p => p.unshift' 0)^[n] p = q
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
rw [hq] at h
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
hq : (fun p => p.unshift' 0)^[n] p = q
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
hq : (fun p => p.unshift' 0)^[n] p = q
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
clear hq
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
⊢ ∀ (i : ℕ), (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
intro i
State after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
i : ℕ
⊢ (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))

State before:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
i : ℕ
⊢ (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
Tactic:
induction' i with i _
State after:
case succ.zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
⊢ (q.unshift' 0).coeff 0 = if 0 < n + 1 then 0 else p.coeff (0 - (n + 1))

case succ.succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
i : ℕ
a✝ : (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
⊢ (q.unshift' 0).coeff (i + 1) = if i + 1 < n + 1 then 0 else p.coeff (i + 1 - (n + 1))

State before:
case succ.zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
⊢ (q.unshift' 0).coeff 0 = if 0 < n + 1 then 0 else p.coeff (0 - (n + 1))
Tactic:
simp only [FormalMultilinearSeries.unshift_coeff_zero, Nat.succ_pos', if_true]
State after:
no goals

State before:
case succ.succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
q : FormalMultilinearSeries 𝕜 𝕜 E
h : ∀ (i : ℕ), q.coeff i = if i < n then 0 else p.coeff (i - n)
i : ℕ
a✝ : (q.unshift' 0).coeff i = if i < n + 1 then 0 else p.coeff (i - (n + 1))
⊢ (q.unshift' 0).coeff (i + 1) = if i + 1 < n + 1 then 0 else p.coeff (i + 1 - (n + 1))
Tactic:
simp only [Nat.succ_lt_succ_iff, h i, FormalMultilinearSeries.unshift_coeff_succ,
  Nat.succ_sub_succ_eq_sub]
State after:
no goals