awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
e_f :
  Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (y : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
e_f :
  ∀ (y : E),
    Eq.{u_7 + 1} (α := F₃)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
⊢ Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (y : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)

Tactic:
ext y
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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₂
ξ y : E
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + (x - y)) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
integral_sub_right_eq_self _ y (μ := volume)

Premises used: MeasureTheory.integral_sub_right_eq_self
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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₂
ξ y : E
h :
  ∀ (x : E),
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + (x - y)) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
convert! integral_sub_right_eq_self _ y (μ := volume)

Premises used: MeasureTheory.integral_sub_right_eq_self
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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₂
ξ y x : E
h : x = y + (x - y)
⊢ HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + (x - y)) ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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₂
ξ y x : E
⊢ x = y + (x - y)

Tactic:
simp
-- 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
e_f :
  Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (y : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
        (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)))

Tactic:
congr
-- 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
e_f :
  ∀ (y : E),
    Eq.{u_7 + 1} (α := F₃)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)))
⊢ Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (y : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
        (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
ext y
-- 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₂
ξ y : E
e_f :
  Eq (α := E → F₃)
    (fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (x : E) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
      (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
        (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)))

Tactic:
congr
-- 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₂
ξ y : E
e_f :
  ∀ (x : E),
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
        (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
⊢ Eq (α := E → F₃)
    (fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    fun (x : E) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
      (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
ext x
-- 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₂
ξ y x : E
e_f :
  HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-(inner ℝ y ξ + inner ℝ x ξ)) : Circle)
      ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ + -inner ℝ x ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
      (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
rw [smul_smul, ← AddChar.map_add_eq_mul, inner_add_left]

Premises used: AddChar.map_add_eq_mul, smul_smul, inner_add_left
-- 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₂
ξ y x : E
e_f : -(inner ℝ y ξ + inner ℝ x ξ) = -inner ℝ y ξ + -inner ℝ x ξ
⊢ HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-(inner ℝ y ξ + inner ℝ x ξ)) : Circle)
      ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) =
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ + -inner ℝ x ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)

Tactic:
congr
-- 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₂
ξ y x : E
⊢ -(inner ℝ y ξ + inner ℝ x ξ) = -inner ℝ y ξ + -inner ℝ x ξ

Tactic:
grind
-- 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
e_f :
  Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)))
    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))
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : 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)))

Tactic:
congr