-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem IntegrableOn.continuousOn_smul [T2Space X] [SecondCountableTopologyEither X 𝕜] {g : X → E}
    (hg : IntegrableOn g K μ) {f : X → 𝕜} (hf : ContinuousOn f 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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ ContinuousOn (fun a => ‖f a‖) K

Tactic:
exact continuous_norm.comp_continuousOn hf

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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ AEStronglyMeasurable (fun x => f x • g x) (μ.restrict K)

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

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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f 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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f 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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f 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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f 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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ AEStronglyMeasurable (fun x => f x • g x) (μ.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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ Integrable (fun a => ‖f a‖ * ‖g a‖) (μ.restrict K)

Tactic:
refine IntegrableOn.continuousOn_mul ?_ hg.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 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ ContinuousOn (fun a => ‖f a‖) K