-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
fourierCoeff :
  _root_.fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
fourierCoeff₁ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
fourierCoeff₂ :
  Eq (α := ℂ) (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
fourierCoeff₃ :
  Eq (α := ℂ) (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
⊢ _root_.fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have fourierCoeff₄ : Eq (α := ℂ) (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ))
Tactic: calc
    fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
        ∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]
    -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
    _ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
    -- Swap sum and integral.
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x := by
      refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm
      convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
      exact funext fun n => neK _ _
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x := by
      simp only [mul_comp] at eadd ⊢
      simp_rw [eadd]
    -- Rearrange sum of interval integrals into an integral over `ℝ`.
    _ = ∫ x, e x * f x := by
      suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
      apply integrable_of_summable_norm_Icc
      convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
      simp_rw [mul_comp] at eadd ⊢
      simp_rw [eadd]
      exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
    -- Minor tidying to finish
    _ = 𝓕 (f : ℝ → ℂ) m := by
      rw [fourier_real_eq_integral_exp_smul]
      congr 1 with x : 1
      rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
      congr 2
      push_cast
      ring