awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
have rw : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
Tactic: rw [← Real.rpow_add (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
have e_a : s / 2 + s' / 2 = (s + s') / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
have _ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
Tactic: calc
    _ = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2) := by
      rw [← Real.rpow_add (by positivity)]
    _ = _ := by congr; ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s s' : ℝ
f : 𝓢'(E, F)
x : E
_ :
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
have _₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
Tactic: calc
    _ = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2) := by
      rw [← Real.rpow_add (by positivity)]
    _ = _ := by congr; ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s s' : ℝ
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (besselPotential E F s' ∘SL besselPotential E F s) (besselPotential E F (s + s'))
have h : ∀ (f : 𝓢'(E, F)),
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s' ∘SL besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((besselPotential E F (s + s') : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
Tactic: ext f : 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g ↔
    (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
have mp : (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g → (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
s : ℝ
f g : 𝓢'(E, F)
mp :
  (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g →
    (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
⊢ (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g ↔
    (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
have mpr : (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f → (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
m : E
f : 𝓢'(E, F)
⊢ (besselPotential E F (-1) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (∂_{m} f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))
have rw : HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
    ((fourierMultiplierCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F)) =
  HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
Tactic: rw [lineDeriv_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
m : E
f : 𝓢'(E, F)
⊢ HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F
              (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
                (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))
have e_a : (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
    (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) =
  fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
m : E
f : 𝓢'(E, F)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) =
    fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)
have e_a : ∀ (x : E),
  HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ))
      (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) x =
    (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
have funProp : HasCompactSupport (β := ℝ) fun (a : E) ↦ ‖a‖
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ (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))
have 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))
Tactic: rw [laplacian_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ 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))
have 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)) : ℂ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ (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)) : ℂ)
have 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)) : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev s p (f + g)
have 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)
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (f + g)
have 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)
Tactic: obtain ⟨g', hg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (f + g)
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f + g) : 𝓢'(E, F))
  (Lp.toTemperedDistribution (f' + g') : 𝓢'(E, F))
Tactic: use f' + g'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev s p (f - g)
have 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)
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (f - g)
have 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)
Tactic: obtain ⟨g', hg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (f - g)
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (f - g) : 𝓢'(E, F))
  (Lp.toTemperedDistribution (f' - g') : 𝓢'(E, F))
Tactic: use f' - g'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev s p (-f)
have 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)
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (-f)
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (-f) : 𝓢'(E, F))
  (Lp.toTemperedDistribution (-f') : 𝓢'(E, F))
Tactic: use -f'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev s p (c • f)
have 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)
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
⊢ MemSobolev s p (c • f)
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (c • f) : 𝓢'(E, F))
  (Lp.toTemperedDistribution (c • f') : 𝓢'(E, F))
Tactic: use c • f'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s p 0
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) 0)
  (Lp.toTemperedDistribution (μ := volume) (p := p) 0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s p
    ((SchwartzMap.toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f)
have 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))
Tactic: use (SchwartzMap.fourierMultiplierCLM F (fun x ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) f).toLp p
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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))
    ((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))
have 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))
Tactic: rw [besselPotential, Lp.toTemperedDistribution_toLp_eq,
    fourierMultiplierCLM_toTemperedDistributionCLM_eq (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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.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))
have 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))
Tactic: congr 1