Theorem: FormalMultilinearSeries.unshift_coeff_succ (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
c : E
n : ℕ
⊢ (p.unshift' c).coeff (n + 1) = p.coeff n
Tactic:
simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.unshift',
  FormalMultilinearSeries.unshift, ContinuousLinearMap.compFormalMultilinearSeries_apply,
  LinearIsometryEquiv.norm_map]
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
c : E
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n 𝕜 E)
        (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E) (ContinuousLinearMap.id 𝕜 𝕜)).compContinuousMultilinearMap (p n)))
      1 =
    (p n) 1

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
c : E
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n 𝕜 E)
        (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E) (ContinuousLinearMap.id 𝕜 𝕜)).compContinuousMultilinearMap (p n)))
      1 =
    (p n) 1
Tactic:
simp [ContinuousLinearMap.smulRightL, Finset.univ, Fintype.elems, Fin.init]
State after:
no goals