awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
⊢ Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (toTemperedDistribution f : 𝓢'(E, F))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, MeasureTheory.Lp.toTemperedDistribution, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
rw :
  ∀ (m : ↥(Lp F p μ)),
    Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) m : 𝓢'(E, F)) (0 : 𝓢'(E, F)) →
      m = 0
⊢ Eq (α := Submodule ℂ ↥(Lp F p μ))
    (LinearMap.ker (M₂ := 𝓢'(E, F)) (↑(toTemperedDistributionCLM F μ p) : ↥(Lp F p μ) →ₗ[ℂ] 𝓢'(E, F))) ⊥

Tactic:
rw [LinearMap.ker_eq_bot', ContinuousLinearMap.coe_coe]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.ker_eq_bot'
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
rw : (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] 0
⊢ f = 0

Tactic:
rw [eq_zero_iff_ae_eq_zero]

Premises used: MeasureTheory.Lp.eq_zero_iff_ae_eq_zero
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
hf₁ : LocallyIntegrable (↑(↑f : E →ₘ[μ] F) : E → F) μ
h :
  ∀ (g : E → ℝ),
    ContDiff ℝ ∞ g → HasCompactSupport g → Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] 0

Tactic:
apply ae_eq_zero_of_integral_contDiff_smul_eq_zero

Premises used: ae_eq_zero_of_integral_contDiff_smul_eq_zero
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
⊢ LocallyIntegrable (↑(↑f : E →ₘ[μ] F) : E → F) μ

Tactic:
(Lp.memLp f).locallyIntegrable hp.elim

Premises used: MeasureTheory.MemLp.locallyIntegrable, MeasureTheory.Lp.memLp, Fact.elim
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
⊢ LocallyIntegrable (↑(↑f : E →ₘ[μ] F) : E → F) μ

Tactic:
exact (Lp.memLp f).locallyIntegrable hp.elim

Premises used: MeasureTheory.MemLp.locallyIntegrable, MeasureTheory.Lp.memLp, Fact.elim
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
⊢ HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)

Tactic:
have hg₁ : HasCompactSupport (Complex.ofRealCLM ∘ g) := g_cpt.comp_left rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)

Tactic:
have hg₂ : ContDiff ℝ ∞ (Complex.ofRealCLM ∘ g) := by fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ : F)
    ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
        (hg₁.toSchwartzMap hg₂) :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ Eq.{u_4 + 1} (α := F)
    ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
        (hg₁.toSchwartzMap hg₂) :
      F)
    (0 : F)

Tactic:
simp [hf]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
_ :
  Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ : F)
    ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
        (hg₁.toSchwartzMap hg₂) :
      F)
_₁ :
  Eq.{u_4 + 1} (α := F)
    ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
        (hg₁.toSchwartzMap hg₂) :
      F)
    (0 : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0

Tactic:
calc
      _ = toTemperedDistributionCLM F μ p f (hg₁.toSchwartzMap hg₂) := by simp
      _ = _ := by simp [hf]

Premises used: MeasureTheory.Lp.toTemperedDistributionCLM, DFunLike.coe, HasCompactSupport.toSchwartzMap
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : E → ℂ
f : 𝓢'(E, F)
f' : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) f' : F)
    ((f : (a : 𝓢(E, ℂ)) → F)
        (((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) f' : 𝓢(E, ℂ)) :
      F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
c : ℂ
f : 𝓢'(E, F)
h :
  ∀ (x : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((smulLeftCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
      ((c • f : (a : 𝓢(E, ℂ)) → F) x : F)
⊢ (smulLeftCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = c • f

Tactic:
ext1
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
c : ℂ
f : 𝓢'(E, F)
x : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
    ((c • f : (a : 𝓢(E, ℂ)) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
h :
  ∀ (x : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((smulLeftCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) ((smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          x :
        F)
      ((((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) ((smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) : 𝓢'(E, F))
    ((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
x : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) ((smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)
    ((((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)

Tactic:
simp [hg₁, hg₂]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢'(E, F)),
    Eq (α := 𝓢'(E, F)) ((smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
      ((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁) (smulLeftCLM F (g₁ * g₂))

Tactic:
ext1 f
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F)) ((smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
simp [hg₁, hg₂]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((((smulLeftCLM F (c • g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (smulLeftCLM F g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.smulLeftCLM_smul hg]

Premises used: SchwartzMap.smulLeftCLM_smul
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((smulLeftCLM F (g₁ + g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((((HAdd.hAdd (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ smulLeftCLM F (g₁ + g₂) = HAdd.hAdd (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂)

Tactic:
ext f u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F (g₁ + g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((HAdd.hAdd (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.smulLeftCLM_add hg₁ hg₂]

Premises used: SchwartzMap.smulLeftCLM_add
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((smulLeftCLM F (g₁ - g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((((HSub.hSub (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ smulLeftCLM F (g₁ - g₂) = HSub.hSub (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂)

Tactic:
ext f u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F (g₁ - g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((HSub.hSub (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.smulLeftCLM_sub hg₁ hg₂]

Premises used: SchwartzMap.smulLeftCLM_sub
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
h :
  ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((((smulLeftCLM F (-g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((((-smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F (-g)) (-smulLeftCLM F g)

Tactic:
ext f u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((((smulLeftCLM F (-g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((-smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [SchwartzMap.smulLeftCLM_neg hg]

Premises used: SchwartzMap.smulLeftCLM_neg
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : ι → E → ℂ
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
h :
  ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
        F)
      ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x) (∑ i ∈ s, smulLeftCLM F (g i))

Tactic:
ext f u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : ι → E → ℂ
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
      F)
    ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [SchwartzMap.smulLeftCLM_sum hg]

Premises used: SchwartzMap.smulLeftCLM_sum
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f))
    ((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f))

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
h :
  Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E),
      HSMul.hSMul (α := ℂ)
        (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
            x :
          ℂ)
        ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
⊢ Eq.{u_4 + 1} (α := F) ((Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
      F)

Tactic:
simp only [Lp.toTemperedDistribution_apply, smulLeftCLM_apply_apply]

Premises used: MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_apply_apply
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
h :
  Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) a : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          a :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) a)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E),
      HSMul.hSMul (α := ℂ)
        (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
            x :
          ℂ)
        ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae