awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᶠ[ae μ] f₂
x : W
a : V
hf' : f₁ a = f₂ a
h h₁ :
  HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a) =
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)
⊢ HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₁ a) =
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)

Tactic:
rw [hf']
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
h : ∀ (w : W), fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
⊢ fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f

Tactic:
ext1 w
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w

Tactic:
simp only [Pi.smul_apply, fourierIntegral, smul_comm _ r, integral_smul]

Premises used: MeasureTheory.integral_smul, VectorFourier.fourierIntegral, SMulCommClass.smul_comm, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

Tactic:
(norm_integral_le_integral_norm _).trans (le_of_eq ?_)

Premises used: MeasureTheory.norm_integral_le_integral_norm, VectorFourier.fourierIntegral, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
refine :
  Eq (α := ℝ)
    (∫ (a : V),
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f a)‖ ∂μ)
    (∫ (v : V), ‖f v‖ ∂μ)
⊢ ‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

Tactic:
refine (norm_integral_le_integral_norm _).trans (le_of_eq ?_)

Premises used: MeasureTheory.norm_integral_le_integral_norm, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ Eq (α := ℝ)
    (∫ (a : V),
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f a)‖ ∂μ)
    (∫ (v : V), ‖f v‖ ∂μ)

Tactic:
simp_rw [Circle.norm_smul]

Premises used: Circle.norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
h :
  ∀ (w : W),
    fourierIntegral e μ L (f ∘ fun (v : V) ↦ v + v₀) w =
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
        (fourierIntegral e μ L f w)
⊢ fourierIntegral e μ L (f ∘ fun (v : V) ↦ v + v₀) = fun (w : W) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
      (fourierIntegral e μ L f w)

Tactic:
ext1 w
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
h :
  ∫ (v : V),
      HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (f (v + v₀)) ∂μ =
    HSMul.hSMul (α := ℂ) (β := E)
      (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (∫ (v : V),
        HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f v) ∂μ)
⊢ fourierIntegral e μ L (f ∘ fun (v : V) ↦ v + v₀) w =
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
      (fourierIntegral e μ L f w)

Tactic:
dsimp only [fourierIntegral, Function.comp_apply, Circle.smul_def]

Premises used: Circle.smul_def, VectorFourier.fourierIntegral, Function.comp_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
rw : ((L : (a : V) → W →ₗ[𝕜] 𝕜) (v + v₀ - v₀) : W →ₗ[𝕜] 𝕜)
| ((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜)

Tactic:
rw [← add_sub_cancel_right v v₀]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
h :
  ∫ (v : V),
      HSMul.hSMul (α := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v + v₀ - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (f (v + v₀)) ∂μ =
    HSMul.hSMul (α := ℂ) (β := E)
      (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (∫ (v : V),
        HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f v) ∂μ)
⊢ ∫ (v : V),
      HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (f (v + v₀)) ∂μ =
    HSMul.hSMul (α := ℂ) (β := E)
      (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (∫ (v : V),
        HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f v) ∂μ)

Tactic:
conv in L _ => rw [← add_sub_cancel_right v v₀]

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
h :
  Eq.{u_4 + 1} (α := E)
    (∫ (x : V),
      HSMul.hSMul (α := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (x - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) (f x) ∂μ)
    (∫ (a : V),
      HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f a)) ∂μ)
⊢ ∫ (v : V),
      HSMul.hSMul (α := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v + v₀ - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (f (v + v₀)) ∂μ =
    HSMul.hSMul (α := ℂ) (β := E)
      (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (∫ (v : V),
        HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f v) ∂μ)

Tactic:
rw [integral_add_right_eq_self fun v : V ↦ (e (-L (v - v₀) w) : ℂ) • f v, ← integral_smul]

Premises used: MeasureTheory.integral_add_right_eq_self, MeasureTheory.integral_smul, HSub.hSub, HSMul.hSMul, Subtype.val, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
h :
  ∀ (v : V),
    HSMul.hSMul (α := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) (f v) =
      HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f v))
⊢ Eq.{u_4 + 1} (α := E)
    (∫ (x : V),
      HSMul.hSMul (α := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (x - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) (f x) ∂μ)
    (∫ (a : V),
      HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
          (f a)) ∂μ)

Tactic:
congr 1 with v
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
⊢ Continuous[inst_10, _] fun (v : V) ↦ (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x)

Tactic:
have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c :
  Continuous[inst_10, _] fun (v : V) ↦ (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x)
simp_rw : Integrable (ε := ℝ) (fun (a : V) ↦ ‖g a‖) μ
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (g v))
    μ

Tactic:
simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]

Premises used: MeasureTheory.integrable_norm_iff, And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul, Circle.norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c :
  Continuous[inst_10, _] fun (v : V) ↦ (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x)
⊢ Integrable (ε := ℝ) (fun (a : V) ↦ ‖g a‖) μ

Tactic:
hg.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c :
  Continuous[inst_10, _] fun (v : V) ↦ (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x)
⊢ Integrable (ε := ℝ) (fun (a : V) ↦ ‖g a‖) μ

Tactic:
exact hg.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
⊢ ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ

Tactic:
have aux {g : V → E} (hg : Integrable g μ) (x : W) :
      Integrable (fun v : V ↦ e (-L v x) • g v) μ := by
    have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
    simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]
    exact hg.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
⊢ Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v))
      μ ↔
    Integrable f μ

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
refine :
  ∀
    (hf :
      Integrable.{u_4, u_2} (ε := E)
        (fun (v : V) ↦
          HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
            (f v))
        μ),
    Integrable f μ
⊢ Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v))
      μ ↔
    Integrable f μ

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
hf :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) (-w)) : 𝕊)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v)))
    μ

Tactic:
have := aux hf (-w)
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
hf :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ
this :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) (-w)) : 𝕊)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v)))
    μ
⊢ Integrable.{u_4, u_2} (ε := E) (fun (v : V) ↦ f v) μ

Tactic:
simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_eq_mul, map_neg, neg_add_cancel,
    e.map_zero_eq_one, one_smul] at this

Premises used: AddChar.map_add_eq_mul, AddChar.map_zero_eq_one, map_neg, one_smul, neg_add_cancel, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
hf :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ
this : Integrable.{u_4, u_2} (ε := E) (fun (v : V) ↦ f v) μ
⊢ Integrable f μ

Tactic:
this