-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this :
  ∀ (x : ℝ),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
      (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
        (↑x : ℝ ⧸ AddSubgroup.zmultiples T)
rw :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
          (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
rw₁ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : AddCircle T) ↦
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ) (f b))
rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (b : AddCircle T),
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
          (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₃ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₄ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) T
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₅ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) ((1 / T) • T)
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₆ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T * T)
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₇ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (α := ℝ) (β := E) 1
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
⊢ fourierCoeff f n =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
          (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
have rw₈ : Eq.{u_1 + 1} (α := E)
  (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
  (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
Tactic: rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
    volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]