awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
⊢ 0 ≤
    ((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
            (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
          HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
      2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
refine_4 :
  ∀ (f : 𝓢(V, E)) (x : V),
    ‖x‖ ^ (k, n).1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
          (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
      HMul.hMul (β := ℝ)
        (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
                (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
              HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(V, E)) (x : V),
        ‖x‖ ^ (k, n).1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
              (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 V E) : (a : 𝓢(V, E)) → ℝ) f : ℝ)

Tactic:
refine ⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
      (2 * π) ^ n * (2 * n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
        2 ^ integrablePower (volume : Measure V) *
        (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2, by positivity,
      fun f x ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
refine_4 :
  ((2 * π) ^ (k, n).2 * (HMul.hMul (α := ℝ) 2 (↑(k, n).2 : ℝ) + 2) ^ (k, n).1 *
      ∑ p ∈ Finset.range ((k, n).2 + 1) ×ˢ Finset.range ((k, n).1 + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
⊢ ‖x‖ ^ (k, n).1 *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
        (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)

Tactic:
apply (pow_mul_norm_iteratedFDeriv_fourier_le (f.smooth ⊤)
      (fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans

Premises used: Real.pow_mul_norm_iteratedFDeriv_fourier_le, MeasureTheory.MeasureSpace.volume, le_top, LE.le.trans, Top.top, SchwartzMap.smooth, SchwartzMap.integrable_pow_mul_iteratedFDeriv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
refine_4 :
  (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ((↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
          (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
                HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
              HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
                (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                        (schwartzSeminormFamily 𝕜 V E) :
                      (a : 𝓢(V, E)) → ℝ)
                    f :
                  ℝ)))))
⊢ ((2 * π) ^ (k, n).2 * (HMul.hMul (α := ℝ) 2 (↑(k, n).2 : ℝ) + 2) ^ (k, n).1 *
      ∑ p ∈ Finset.range ((k, n).2 + 1) ×ˢ Finset.range ((k, n).1 + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
refine_4 :
  (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
      (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
            (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                    (schwartzSeminormFamily 𝕜 V E) :
                  (a : 𝓢(V, E)) → ℝ)
                f :
              ℝ)))
⊢ (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ((↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
          (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
                HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
              HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
                (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                        (schwartzSeminormFamily 𝕜 V E) :
                      (a : 𝓢(V, E)) → ℝ)
                    f :
                  ℝ)))))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
h :
  ∀ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
      HMul.hMul (β := ℝ)
        ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ)
⊢ LE.le (α := ℝ)
    (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v))
    (∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      HMul.hMul (β := ℝ)
        ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ))

Tactic:
gcongr with p
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h_1 : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
h :
  (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
        @integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
        ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      ‖v‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)

Tactic:
apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans

Premises used: SchwartzMap.integral_pow_mul_iteratedFDeriv_le, LE.le.trans
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h_1 : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
h :
  HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
      ((@integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
          ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)) ≤
    HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ))
⊢ (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
        @integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
        ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)

Tactic:
simp only [mul_assoc, two_mul]

Premises used: mul_assoc, two_mul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h_1 : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
h :
  LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
h₁ :
  LE.le (α := ℝ)
    ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
⊢ HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
      ((@integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
          ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)) ≤
    HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (0, p.2) ∈ Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (0, p.2) ∈ Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)

Tactic:
have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
this : (0, p.2) ∈ Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)
⊢ LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)

Tactic:
apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)

Premises used: Seminorm.le_def, Iff.mp, Finset.le_sup
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (p.1 + integrablePower.{u_3} (E := V) volume, p.2) ∈
    Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (p.1 + integrablePower.{u_3} (E := V) volume, p.2) ∈
    Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)

Tactic:
have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all