awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
x : E
h : HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 0 = 1
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + -s / 2) = 1

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
x : E
⊢ HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 0 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
rw :
  ∀
    (hf :
      ∃ (f' : ↥(Lp F 2 volume)),
        Eq (α := 𝓢'(E, F))
          ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
              (𝓕 f) :
            𝓢'(E, F))
          (Lp.toTemperedDistribution f' : 𝓢'(E, F)))
    {g : E → ℂ} (hg₁ : Function.HasTemperateGrowth g) (hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C),
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)

Tactic:
rw [memSobolev_iff_exists_smulLeftCLM_fourier] at hf ⊢

Premises used: TemperedDistribution.memSobolev_iff_exists_smulLeftCLM_fourier
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf :
  ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
obtain :
  ∀ (f' : ↥(Lp F 2 volume))
    (hf :
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))),
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))

Tactic:
obtain ⟨f', hf⟩ := hf
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
obtain :
  ∀ (C : ℝ) (hC : ∀ (x : E), ‖g x‖ ≤ C),
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))

Tactic:
obtain ⟨C, hC⟩ := hg₂
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
h :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (HSMul.hSMul (α := ↥(Lp ℂ ∞ volume)) (MemLp.toLp (⇑g' : (a : E) → ℂ) ⋯) f') : 𝓢'(E, F))
⊢ ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))

Tactic:
use (g'.memLp_top.toLp _ (μ := volume)) • f'

Premises used: BoundedContinuousFunction.memLp_top, MeasureTheory.MemLp.toLp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ Function.HasTemperateGrowth (E := E) (F := ℂ) (⇑g' : (a : E) → ℂ)

Tactic:
apply hg₁
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
h :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
    ((smulLeftCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
              (⇑g' : (a : E) → ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (HSMul.hSMul (α := ↥(Lp ℂ ∞ volume)) (MemLp.toLp (⇑g' : (a : E) → ℂ) ⋯) f') : 𝓢'(E, F))

Tactic:
rw [MeasureTheory.Lp.toTemperedDistribution_smul_eq (by apply hg₁), ← hf,
    fourierMultiplierCLM_apply, fourier_fourierInv_eq,
    smulLeftCLM_smulLeftCLM_apply hg₁ (by fun_prop),
    smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by apply hg₁)]

Premises used: TemperedDistribution.fourierMultiplierCLM_apply, FourierInvPair.fourier_fourierInv_eq, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
h :
  (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) =
    HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) (⇑g' : (a : E) → ℂ)
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
    ((smulLeftCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
              (⇑g' : (a : E) → ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))

Tactic:
congr 2
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
h :
  ∀ (x : E),
    HMul.hMul (β := E → ℂ) g (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) x =
      HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
        (⇑g' : (a : E) → ℂ) x
⊢ (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) =
    HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) (⇑g' : (a : E) → ℂ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
x : E
h :
  HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) g x =
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (⇑g' : (a : E) → ℂ) x
⊢ HMul.hMul (β := E → ℂ) g (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) x =
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (⇑g' : (a : E) → ℂ) x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
x : E
⊢ HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) g x =
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (⇑g' : (a : E) → ℂ) x

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ LT.lt (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
rw : s' - s ≤ HMul.hMul (α := ℝ) 0 2
⊢ (s' - s) / 2 ≤ 0

Tactic:
rw [div_le_iff₀ (by norm_num)]

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ s' - s ≤ HMul.hMul (α := ℝ) 0 2

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ (s' - s) / 2 ≤ 0

Tactic:
have h' : (s' - s) / 2 ≤ 0 := by
    rw [div_le_iff₀ (by norm_num)]
    simp [h]
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
⊢ s' = s' - s + s

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
⊢ s' = s' - s + s

Tactic:
have hs : s' = (s' - s) + s := by ring
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
rw : MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((besselPotential E F (s' - s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)
⊢ MemSobolev s' 2 f

Tactic:
rw [hs, ← memSobolev_besselPotential_iff]

Premises used: TemperedDistribution.memSobolev_besselPotential_iff
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
apply : ∃ (C : ℝ), ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ C
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((besselPotential E F (s' - s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)

Tactic:
apply hf.fourierMultiplierCLM_of_bounded (by fun_prop)

Premises used: TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
h₁ : ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ 1
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ C

Tactic:
use 1
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ 0 ≤ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
h₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2) ≤ 1
⊢ ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ 1

Tactic:
rw [Complex.norm_real, Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]

Premises used: Iff.mpr, Complex.norm_real, abs_eq_self, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ 1 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2) ≤ 1

Tactic:
exact Real.rpow_le_one_of_one_le_of_nonpos (by simp) h'

Premises used: Real.rpow_le_one_of_one_le_of_nonpos