-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
rw :
  Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            (B : (a : F₁) → F₂ →L[ℂ] F₃)
              (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      ((B : (a : F₁) → F₂ →L[ℂ] F₃)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₂ x)))
rw₁ rw₂ :
  Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            (B : (a : F₁) → F₂ →L[ℂ] F₃)
              (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            (B : (a : F₁) → F₂ →L[ℂ] F₃)
              (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₂ x)))
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              (B : (a : F₁) → F₂ →L[ℂ] F₃)
                (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
            (a : F₂) → F₃)
          (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) :
      F₃)
    (((B : (a : F₁) → F₂ →L[ℂ] F₃)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) :
      F₃)

Tactic:
rw [← integral_comp_comm _ (by simpa using hf₂), ← integral_comp_comm _ (by simpa using hf₁)]

Premises used: ContinuousLinearMap.integral_comp_comm