-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem IntegrableOn.smul_continuousOn [T2Space X] [SecondCountableTopologyEither X E] {f : X → 𝕜}
    (hf : IntegrableOn f K μ) {g : X → E} (hg : ContinuousOn g K) (hK : IsCompact K) :
    IntegrableOn (fun x => f x • g x) K μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ Integrable (fun a => ‖f a • g a‖) (μ.restrict K)

Tactic:
simp_rw [norm_smul]

Result:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ Integrable (fun a => ‖f a‖ * ‖g a‖) (μ.restrict K)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ ContinuousOn (fun a => ‖g a‖) K

Tactic:
exact continuous_norm.comp_continuousOn hg

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ Integrable (fun a => ‖f a‖ * ‖g a‖) (μ.restrict K)

Tactic:
refine IntegrableOn.mul_continuousOn hf.norm ?_ hK

Result:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ ContinuousOn (fun a => ‖g a‖) K

Proof state:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ AEStronglyMeasurable (fun x => f x • g x) (μ.restrict K)

Tactic:
exact hf.1.smul (hg.aestronglyMeasurable hK.measurableSet)

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ IntegrableOn (fun x => f x • g x) K μ

Tactic:
rw [IntegrableOn, ← integrable_norm_iff]

Result:
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ Integrable (fun a => ‖f a • g a‖) (μ.restrict K)

X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : T2Space X
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ AEStronglyMeasurable (fun x => f x • g x) (μ.restrict K)