partialFourierSum_eq_partialFourierSum'

lemma partialFourierSum_eq_partialFourierSum' (N : ℕ) (f : ℝ → ℂ) :    liftIoc (2 * π) 0 (partialFourierSum N f)      = partialFourierSum' N (liftIoc (2 * π) 0 f) := by  ext x  unfold partialFourierSum partialFourierSum' liftIoc  simp only [    Function.comp_apply, Set.restrict_apply, Int.ofNat_eq_natCast, ContinuousMap.coe_sum,    ContinuousMap.coe_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]  congr with n  rw [← liftIoc, fourierCoeff_liftIoc_eq]  congr 2  · rw [zero_add (2 * π)]  · rcases (eq_coe_Ioc x) with ⟨b, hb, rfl⟩    rw [← zero_add (2 * π)] at hb    rw [coe_eq_coe_iff_of_mem_Ioc (Subtype.coe_prop _) hb]    have : (liftIoc (2 * π) 0 (fun x ↦ x)) b = (fun x ↦ x) b := liftIoc_coe_apply hb    unfold liftIoc at this    rw [Function.comp_apply, Set.restrict_apply] at this    exact this