Theorem: unevenSeries_apply (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
z1 : ℂ
n : ℕ
⊢ ((unevenSeries' u r z1 n) fun x => 1) = unevenTerm' u r z1 n
Tactic:
simp only [unevenSeries', ContinuousMultilinearMap.mkPiRing_apply, Finset.prod_const_one,
  one_smul]
State after:
no goals