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 : NormedSpace ℂ F
f : 𝓢'(E, F)
rw :
  HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F
              (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)) fun (x : E) ↦
                (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)) =
    HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))
⊢ (besselPotential E F (-2) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Δ f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))

Tactic:
rw [laplacian_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]

Premises used: ContinuousLinearMap.map_smul_of_tower, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, TemperedDistribution.besselPotential
-- 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 : NormedSpace ℂ F
f : 𝓢'(E, F)
e_a :
  (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) =
    fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)
⊢ HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F
              (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)) fun (x : E) ↦
                (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)) =
    HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))

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 : NormedSpace ℂ F
f : 𝓢'(E, F)
e_a :
  ∀ (x : E),
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ))
        (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) x =
      (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) =
    fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)

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 : NormedSpace ℂ F
f : 𝓢'(E, F)
x : E
⊢ HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ))
      (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)) x =
    (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-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
s : ℝ
f : 𝓢'(E, F)
⊢ 𝓕 (E := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f)

Tactic:
simp [besselPotential, fourierMultiplierCLM]

Premises used: TemperedDistribution.fourierMultiplierCLM, TemperedDistribution.besselPotential
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
⊢ MemSobolev 0 p f ↔ ∃ (f' : ↥(Lp F p volume)), f = Lp.toTemperedDistribution f'

Tactic:
simp [MemSobolev]

Premises used: TemperedDistribution.MemSobolev
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
hf : MemSobolev s p f
hg : MemSobolev s p g
obtain :
  ∀ (f' : ↥(Lp F p volume))
    (hf :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))),
    MemSobolev s p (f + g)
⊢ MemSobolev s p (f + g)

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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
hg : MemSobolev s p g
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
obtain :
  ∀ (g' : ↥(Lp F p volume))
    (hg :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
        (Lp.toTemperedDistribution g' : 𝓢'(E, F))),
    MemSobolev s p (f + g)
⊢ MemSobolev s p (f + g)

Tactic:
obtain ⟨g', hg⟩ := 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
g' : ↥(Lp F p volume)
hg :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
    (Lp.toTemperedDistribution g' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f + g) : 𝓢'(E, F))
    (Lp.toTemperedDistribution (f' + g') : 𝓢'(E, F))
⊢ MemSobolev s p (f + g)

Tactic:
use f' + g'
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
g' : ↥(Lp F p volume)
hg :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
    (Lp.toTemperedDistribution g' : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f + g) : 𝓢'(E, F))
    ((Lp.toTemperedDistributionCLM F volume p : (a : ↥(Lp F p volume)) → 𝓢'(E, F)) (f' + g') : 𝓢'(E, F))

Tactic:
simp [map_add, hf, hg]

Premises used: map_add
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
hf : MemSobolev s p f
hg : MemSobolev s p g
obtain :
  ∀ (f' : ↥(Lp F p volume))
    (hf :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))),
    MemSobolev s p (f - g)
⊢ MemSobolev s p (f - g)

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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
hg : MemSobolev s p g
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
obtain :
  ∀ (g' : ↥(Lp F p volume))
    (hg :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
        (Lp.toTemperedDistribution g' : 𝓢'(E, F))),
    MemSobolev s p (f - g)
⊢ MemSobolev s p (f - g)

Tactic:
obtain ⟨g', hg⟩ := 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
g' : ↥(Lp F p volume)
hg :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
    (Lp.toTemperedDistribution g' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f - g) : 𝓢'(E, F))
    (Lp.toTemperedDistribution (f' - g') : 𝓢'(E, F))
⊢ MemSobolev s p (f - g)

Tactic:
use f' - g'
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
g' : ↥(Lp F p volume)
hg :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g : 𝓢'(E, F))
    (Lp.toTemperedDistribution g' : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f - g) : 𝓢'(E, F))
    ((Lp.toTemperedDistributionCLM F volume p : (a : ↥(Lp F p volume)) → 𝓢'(E, F)) (f' - g') : 𝓢'(E, F))

Tactic:
simp [map_sub, hf, hg]

Premises used: map_sub
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
hf : MemSobolev s p f
obtain :
  ∀ (f' : ↥(Lp F p volume))
    (hf :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))),
    MemSobolev s p (-f)
⊢ MemSobolev s p (-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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (-f) : 𝓢'(E, F))
    (Lp.toTemperedDistribution (-f') : 𝓢'(E, F))
⊢ MemSobolev s p (-f)

Tactic:
use -f'
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (-f) : 𝓢'(E, F))
    ((Lp.toTemperedDistributionCLM F volume p : (a : ↥(Lp F p volume)) → 𝓢'(E, F)) (-f') : 𝓢'(E, F))

Tactic:
simp [map_neg, hf]

Premises used: map_neg
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
hf : MemSobolev s p f
obtain :
  ∀ (f' : ↥(Lp F p volume))
    (hf :
      Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))),
    MemSobolev s p (c • f)
⊢ MemSobolev s p (c • 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (c • f) : 𝓢'(E, F))
    (Lp.toTemperedDistribution (c • f') : 𝓢'(E, F))
⊢ MemSobolev s p (c • f)

Tactic:
use c • f'
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (c • f) : 𝓢'(E, F))
    ((Lp.toTemperedDistributionCLM F volume p : (a : ↥(Lp F p volume)) → 𝓢'(E, F)) (c • f') : 𝓢'(E, F))

Tactic:
simp [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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) 0)
    (Lp.toTemperedDistribution (μ := volume) (p := p) 0)
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s p 0

Tactic:
use 0
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) 0)
    ((Lp.toTemperedDistributionCLM F volume p : (a : ↥(Lp F p volume)) → 𝓢'(E, F)) 0)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s r : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s p ((besselPotential E F r : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) ↔
    MemSobolev (r + s) p f

Tactic:
simp [MemSobolev]

Premises used: TemperedDistribution.MemSobolev
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
h :
  Eq (α := 𝓢'(E, F))
    ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (μ := volume)
        (SchwartzMap.toLp
          (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
                𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → 𝓢(E, F))
            f)
          p volume) :
      𝓢'(E, F))
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s p
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f)

Tactic:
use (SchwartzMap.fourierMultiplierCLM F (fun x ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) f).toLp p

Premises used: Norm.norm, HDiv.hDiv, SchwartzMap.fourierMultiplierCLM, HPow.hPow, HAdd.hAdd, SchwartzMap.toLp, OfNat.ofNat, DFunLike.coe
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
h :
  Eq (α := 𝓢'(E, F))
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F))
        (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
              𝓢(E, F) →L[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f) :
      𝓢'(E, F))
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F))
        (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
              𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f) :
      𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F))
    ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (μ := volume)
        (SchwartzMap.toLp
          (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
                𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → 𝓢(E, F))
            f)
          p volume) :
      𝓢'(E, F))

Tactic:
rw [besselPotential, Lp.toTemperedDistribution_toLp_eq,
    fourierMultiplierCLM_toTemperedDistributionCLM_eq (by fun_prop)]

Premises used: TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.besselPotential
-- 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
h :
  Eq (α := 𝓢(E, F))
    (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
            𝓢(E, F) →L[ℂ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
            𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
⊢ Eq (α := 𝓢'(E, F))
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F))
        (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
              𝓢(E, F) →L[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f) :
      𝓢'(E, F))
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F))
        (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
              𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f) :
      𝓢'(E, F))

Tactic:
congr 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 : NormedSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
            𝓢(E, F) →L[ℂ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((SchwartzMap.fourierMultiplierCLM F fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) :
            𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))

Tactic:
apply SchwartzMap.fourierMultiplierCLM_ofReal ℂ
    (Function.hasTemperateGrowth_one_add_norm_sq_rpow E (s / 2))

Premises used: HDiv.hDiv, SchwartzMap.fourierMultiplierCLM_ofReal, Complex, OfNat.ofNat, Function.hasTemperateGrowth_one_add_norm_sq_rpow