-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
H₃ :
  HPow.hPow (β := ℕ) ‖f‖ 2 =
    ∫ (x : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle
rwa :
  ∀
    (H₁ :
      HasSum
        (fun (i : ℤ) ↦
          HPow.hPow (β := ℕ)
            (norm (E := (fun (x : ℤ) ↦ ℂ) i)
              ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
                  (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
                i))
            2)
        (HPow.hPow (β := ℕ) ‖f‖ 2))
    (H₂ :
      HPow.hPow (β := ℕ)
          (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
            ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
              ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
          2 =
        HPow.hPow (β := ℕ) ‖f‖ 2)
    (H₃ :
      HPow.hPow (β := ℕ) ‖f‖ 2 =
        ∫ (x : AddCircle T),
          HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle),
    HasSum (α := ℝ)
      (fun (i : ℤ) ↦
        HPow.hPow (β := ℕ)
          (norm (E := ℂ)
            ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
                (i : ℤ) → ℂ)
              i))
          2)
      (∫ (t : AddCircle T),
        HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have rwa₁ : ∀
  (H₁ :
    HasSum (α := ℝ)
      (fun (i : ℤ) ↦
        HPow.hPow (β := ℕ)
          (norm (E := (fun (x : ℤ) ↦ ℂ) i)
            ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
                (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
              i))
          2)
      (∫ (x : AddCircle T),
        HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle))
  (H₂ :
    HPow.hPow (β := ℕ)
        (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
          ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
            ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
        2 =
      HPow.hPow (β := ℕ) ‖f‖ 2)
  (H₃ :
    HPow.hPow (β := ℕ) ‖f‖ 2 =
      ∫ (x : AddCircle T),
        HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle),
  HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
Tactic: rwa [H₂, H₃] at H₁
Cleared hypotheses: H₁, H₂, H₃