chore(FunProp): additional lemmas for Integrable (leanprover-community#39326)

Done at ICERM workshop "Techniques and Tools for the Formalization of Analysis".

Author: mcdoll

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

@@ -1128,6 +1128,7 @@ lemma integrable_pow_mul (f : 𝓢(D, V))
   convert integrable_pow_mul_iteratedFDeriv μ f k 0 with x
   simp
 
+@[fun_prop]
 lemma integrable (f : 𝓢(D, V)) : Integrable f μ :=
   (f.integrable_pow_mul μ 0).mono f.continuous.aestronglyMeasurable
     (Eventually.of_forall (fun _ ↦ by simp))

Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean

@@ -100,7 +100,7 @@ end AEEqFun
 
 namespace L1
 
-
+@[fun_prop]
 theorem integrable_coeFn (f : α →₁[μ] β) : Integrable f μ := by
   rw [← memLp_one_iff_integrable]
   exact Lp.memLp f

Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

@@ -1038,6 +1038,7 @@ theorem Integrable.const_mul {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜)
     Integrable (fun x => c * f x) μ :=
   h.smul c
 
+@[fun_prop]
 theorem Integrable.const_mul' {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
     Integrable ((fun _ : α => c) * f) μ :=
   Integrable.const_mul h c
@@ -1047,6 +1048,7 @@ theorem Integrable.mul_const {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜)
     Integrable (fun x => f x * c) μ :=
   h.smul (MulOpposite.op c)
 
+@[fun_prop]
 theorem Integrable.mul_const' {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
     Integrable (f * fun _ : α => c) μ :=
   Integrable.mul_const h c

Mathlib/MeasureTheory/Integral/Prod.lean

@@ -337,12 +337,14 @@ lemma Integrable.comp_snd {f : β → E} (hf : Integrable f ν) (μ : Measure α
   exact hf.comp_snd μ
 
 omit [SFinite ν] in
+@[fun_prop]
 theorem Integrable.smul_prod {R : Type*} [NormedRing R] [Module R E] [IsBoundedSMul R E]
     {f : α → R} {g : β → E} (hf : Integrable f μ) (hg : Integrable g ν) :
     Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν) :=
   hf.op_fst_snd continuous_smul ⟨1, by simpa using norm_smul_le⟩ hg
 
 omit [SFinite ν] in
+@[fun_prop]
 theorem Integrable.mul_prod {L : Type*} [NormedRing L] {f : α → L} {g : β → L} (hf : Integrable f μ)
     (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 * g z.2) (μ.prod ν) :=
   hf.smul_prod hg