awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
h :
  ∀ (w : StrongDual ℝ V),
    Eq.{u_1 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
      (((fun (w : V) ↦
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
          (⇑A : (a : StrongDual ℝ V) → V))
        w)
⊢ Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))

Tactic:
ext1 w
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
h :
  ∀ (v : V),
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    (((fun (w : V) ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
        (⇑A : (a : StrongDual ℝ V) → V))
      w)

Tactic:
congr 1 with v : 1
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
v : V
h :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(starRingEnd ℝ : (a : ℝ) → ℝ) ⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
h₁ :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
h₂ h₃ :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)

Tactic:
rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]

Premises used: InnerProductSpace.toDual_symm_apply, RCLike.conj_to_real, inner_conj_symm
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
⊢ Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))

Tactic:
have : (fun w : StrongDual ℝ V ↦ ∫ v, 𝐞 (-w v) • f v) =
      (fun w : V ↦ ∫ v, 𝐞 (-⟪v, w⟫) • f v) ∘ A := by
    ext1 w
    congr 1 with v : 1
    rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
this :
  Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
hf :
  Tendsto.{u_2, u_1} (α := StrongDual ℝ V) (β := E)
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (x : StrongDual ℝ V) ↦
      @integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(x : (a : V) → ℝ) v) : Circle) (f v))
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
this :
  Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
⊢ Tendsto.{u_2, u_1} (α := StrongDual ℝ V) (β := E)
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
(tendsto_integral_exp_inner_smul_cocompact f).comp
      A.toHomeomorph.toCocompactMap.cocompact_tendsto'

Premises used: LinearIsometryEquiv.toHomeomorph, Homeomorph.toCocompactMap, CocompactMap.cocompact_tendsto', tendsto_integral_exp_inner_smul_cocompact, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
have :
  ∀ (A : V ≃L[ℝ] V'),
    Tendsto.{u_2, u_1} (β := E)
      (fun (w : StrongDual ℝ V) ↦
        ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
      (cocompact (StrongDual ℝ V)) (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
have A : V ≃L[ℝ] V' := toEuclidean
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
⊢ let this := borel V';
  BorelSpace V'

Tactic:
borelize V'
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this : MeasurableSpace V' := borel V'
this_1 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
⊢ Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)

Tactic:
have : (μ.map Aₘ).IsAddHaarMeasure := A.isAddHaarMeasure_map _
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
⊢ Tendsto.{u_2, u_1} (β := E)
    ((fun (w : StrongDual ℝ V') ↦
        @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
            ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
      Adual.toHomeomorph.toCocompactMap.toFun)
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
(tendsto_integral_exp_smul_cocompact_of_inner_product (f ∘ A.symm) (μ.map Aₘ)).comp
      Adual.toHomeomorph.toCocompactMap.cocompact_tendsto'

Premises used: Homeomorph.toCocompactMap, ContinuousLinearEquiv.symm, CocompactMap.cocompact_tendsto', Function.comp, tendsto_integral_exp_smul_cocompact_of_inner_product, MeasureTheory.Measure.map, ContinuousLinearEquiv.toHomeomorph, Filter.Tendsto.comp, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
h :
  ∀ (w : StrongDual ℝ V),
    Eq.{u_1 + 1} (α := E)
      (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
      (((fun (w : StrongDual ℝ V') ↦
            @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
                ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
          Adual.toHomeomorph.toCocompactMap.toFun)
        w)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
convert!
    (tendsto_integral_exp_smul_cocompact_of_inner_product (f ∘ A.symm) (μ.map Aₘ)).comp
      Adual.toHomeomorph.toCocompactMap.cocompact_tendsto' with
    w

Premises used: Homeomorph.toCocompactMap, ContinuousLinearEquiv.symm, CocompactMap.cocompact_tendsto', Function.comp, tendsto_integral_exp_smul_cocompact_of_inner_product, MeasureTheory.Measure.map, ContinuousLinearEquiv.toHomeomorph, Filter.Tendsto.comp, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this_3 : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
w : StrongDual ℝ V
this :
  Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (∫ (x : V),
      HSMul.hSMul (α := Circle)
        ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V') : V)) :
          Circle)
        (f ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V'))) ∂μ)
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (((fun (w : StrongDual ℝ V') ↦
          @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
              ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
        Adual.toHomeomorph.toCocompactMap.toFun)
      w)

Tactic:
simpa [Function.comp_apply, integral_map_equiv, Adual]

Premises used: MeasureTheory.integral_map_equiv, Function.comp_apply
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
w : StrongDual ℝ V
h :
  Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (∫ (x : V),
      HSMul.hSMul (α := Circle)
        ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V') : V)) :
          Circle)
        (f ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V'))) ∂μ)
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (((fun (w : StrongDual ℝ V') ↦
          @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
              ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
        Adual.toHomeomorph.toCocompactMap.toFun)
      w)

Tactic:
suffices ∫ v, 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-w (A.symm (Aₘ x))) • f (A.symm (Aₘ x)) ∂μ by
    simpa [Function.comp_apply, integral_map_equiv, Adual]
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
w : StrongDual ℝ V
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (∫ (x : V),
      HSMul.hSMul (α := Circle)
        ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V') : V)) :
          Circle)
        (f ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V'))) ∂μ)

Tactic:
simp [Aₘ]
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
⊢ Tendsto (α := V →L[ℝ] ℝ) (VectorFourier.fourierIntegral 𝐞 μ (LinearMap.flip (topDualPairing ℝ V)) f)
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
_root_.tendsto_integral_exp_smul_cocompact f μ

Premises used: tendsto_integral_exp_smul_cocompact, VectorFourier.fourierIntegral
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
f : ((i : ι) → A i) → ℝ≥0∞
x : (i : ι) → A i
⊢ T (A := A) μ p f Finset.univ x =
    ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (t : A i), f (update (β := A) x i t) ∂μ i) ^ p ∂Measure.pi (α := A) μ

Tactic:
simp [T, lmarginal_singleton]

Premises used: MeasureTheory.GridLines.T, MeasureTheory.lmarginal_singleton
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
f : ((i : ι) → A i) → ℝ≥0∞
x : (i : ι) → A i
⊢ T (A := A) μ p f ∅ x = f x ^ (1 + p)

Tactic:
simp [T]

Premises used: MeasureTheory.GridLines.T
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
simp_rw :
  lmarginal (X := A) μ (insert i s)
      (f ^ (1 - HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p) =
    lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p)
⊢ T (A := A) μ p f (insert i s) =
    lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p)

Tactic:
simp_rw [T, card_insert_of_notMem hi]

Premises used: MeasureTheory.GridLines.T, Finset.card_insert_of_notMem
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 = (↑(#s) : ℝ)
⊢ lmarginal (X := A) μ (insert i s)
      (f ^ (1 - HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p) =
    lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p)

Tactic:
congr!
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 - 1 = (↑(#s) : ℝ)
⊢ HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 = (↑(#s) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 - 1 = (↑(#s) : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
rw :
  (lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (xᵢ : A i),
        HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
          (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) (update (β := A) x i xᵢ) ∂μ i) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i
rw₁ : Measurable (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p)
⊢ lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i

Tactic:
rw [lmarginal_insert' _ _ hi]

Premises used: MeasureTheory.lmarginal_insert'