-- 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
simp_rw :
  HSMul.hSMul (β := ℂ) (1 / 1)
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
simp_rw₁ :
  HSMul.hSMul (α := ℝ) (β := ℂ) 1
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
simp_rw₂ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₃ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₄ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ)
        ((ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m))
                { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ : C(ℝ, AddCircle (𝕜 := ℝ) 1) } :
              (a : ℝ) → ℂ)
            x :
          ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₅ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ)
        ((fourier (-m) : (a : AddCircle 1) → ℂ)
            (({ toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ } : (a : ℝ) → AddCircle 1) x :
              AddCircle (𝕜 := ℝ) 1) :
          ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₆ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₇ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) (β := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
⊢ 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 : ℂ)
have simp_rw₈ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HSMul.hSMul (α := ℂ) (β := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
Tactic: 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]