awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ fourierIntegral e μ L f₁ x = fourierIntegral e μ L f₂ x
have h : EventuallyEq.{u_2, u_4} (β := E) (ae μ)
  (fun (a : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₁ a))
  fun (a : V) ↦
  HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae μ)
    (fun (a : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
        (f₁ a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)
have h : ∀ (a : V) (hf' : f₁ a = 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: filter_upwards [hf] with _ hf'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)
have 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)
Tactic: rw [hf']
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 : ℂ
⊢ fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f
have h : ∀ (w : W), fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
Tactic: ext1 w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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‖ ∂μ
have refine : Eq (α := ℝ)
  (∫ (a : V),
    ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
        (f a)‖ ∂μ)
  (∫ (v : V), ‖f v‖ ∂μ)
Tactic: refine (norm_integral_le_integral_norm _).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)
have 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)
Tactic: ext1 w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)
have 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) ∂μ)
Tactic: dsimp only [fourierIntegral, Function.comp_apply, Circle.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
| ((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜)
have rw : ((L : (a : V) → W →ₗ[𝕜] 𝕜) (v + v₀ - v₀) : W →ₗ[𝕜] 𝕜)
Tactic: rw [← add_sub_cancel_right v v₀]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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),
      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) ∂μ)
have 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) ∂μ)
Tactic: conv in L _ => rw [← add_sub_cancel_right v v₀]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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),
      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) ∂μ)
have 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)) ∂μ)
Tactic: rw [integral_add_right_eq_self fun v : V ↦ (e (-L (v - v₀) w) : ℂ) • f v, ← integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)) ∂μ)
have 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))
Tactic: congr 1 with v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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))
have h : 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)) : ℂ)
      (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
    f v
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
h :
  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)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f 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))
have h₁ : HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
    (f v) =
  HMul.hMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
    f v
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
h :
  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)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₁ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HMul.hMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f 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))
have h₂ : HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
    (f v) =
  (↑(HMul.hMul (α := 𝕊) (β := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)) :
      ℂ) •
    f v
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
h :
  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)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₁ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HMul.hMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₂ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    (↑(HMul.hMul (α := 𝕊) (β := 𝕊)
            ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)) :
        ℂ) •
      f 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))
have h₃ : HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
    (f v) =
  HSMul.hSMul (α := ℂ)
    (↑((e : (a : 𝕜) → 𝕊)
          (HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
            (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
      ℂ)
    (f v)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
h :
  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)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₁ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HMul.hMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₂ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    (↑(HMul.hMul (α := 𝕊) (β := 𝕊)
            ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)) :
        ℂ) •
      f v
h₃ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ)
      (↑((e : (a : 𝕜) → 𝕊)
            (HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
              (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
        ℂ)
      (f 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))
have h₄ : HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (((-(L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
    (f v) =
  HSMul.hSMul (α := ℂ)
    (↑((e : (a : 𝕜) → 𝕊)
          (HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
            (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
      ℂ)
    (f v)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (hypothesis)
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))
    μ
have c : 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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (g v))
    μ
have simp_rw : Integrable (ε := ℝ) (fun (a : V) ↦ ‖g a‖) μ
Tactic: simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]