awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 ℝ 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₃))
have 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₃)
Tactic: convert! integral_sub_right_eq_self _ y (μ := volume)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃)
have h : x = y + (x - y)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃)))
have 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₃))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃))
have 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₃)))
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃)))
have 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₃))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃))
have 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₃))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃))
have 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₃)
Tactic: rw [smul_smul, ← AddChar.map_add_eq_mul, inner_add_left]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃)
have e_f : -(inner ℝ y ξ + inner ℝ x ξ) = -inner ℝ y ξ + -inner ℝ x ξ
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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)))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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))
have e_f : ∀ (y : E),
  Eq.{u_7 + 1} (α := 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₃)) :
      F₃)
    ((@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₃)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ Eq.{u_7 + 1} (α := 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₃)) :
      F₃)
    ((@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₃)
have e_f : HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) =
  HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
    ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
              ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
          (a : F₂) → F₃)
        (f₂ y) :
      F₃)
Tactic: simp_rw [Circle.smul_def, map_smul, MeasureTheory.integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
        HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) =
    HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
                ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
            (a : F₂) → F₃)
          (f₂ y) :
        F₃)
have e_f : Eq.{u_7 + 1} (α := F₃)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) :
    F₃)
  ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
          HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
            ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
        (a : F₂) → F₃)
      (f₂ y) :
    F₃)
Tactic: congr