-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem IntegrableOn.continuousOn_mul_of_subset (hg : ContinuousOn g K) (hg' : IntegrableOn g' A μ)
    (hK : IsCompact K) (hA : MeasurableSet A) (hAK : A ⊆ K) :
    IntegrableOn (fun x => g x * g' x) A μ

Proof state:
case h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x‖ * ‖g' x‖ ≤ C * ‖g' x‖

Tactic:
gcongr

Result:
case h.h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x‖ ≤ C

Proof state:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn (fun x => g x * g' x) A μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable] at hg' ⊢

Result:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ MemLp (fun x => g x * g' x) 1 (μ.restrict A)

Proof state:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
this : ∀ᵐ (x : X) ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖
⊢ MemLp (fun x => g x * g' x) 1 (μ.restrict A)

Tactic:
exact
  MemLp.of_le_mul hg' (((hg.mono hAK).aestronglyMeasurable hA).mul hg'.aestronglyMeasurable) this

Result:
no goals

Proof state:
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
⊢ IntegrableOn (fun x => g x * g' x) A μ

Tactic:
rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩

Result:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn (fun x => g x * g' x) A μ

Proof state:
case h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x * g' x‖ ≤ C * ‖g' x‖

Tactic:
refine (norm_mul_le _ _).trans ?_

Result:
case h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x‖ * ‖g' x‖ ≤ C * ‖g' x‖

Proof state:
case h.h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x‖ ≤ C

Tactic:
exact hC x (hAK hx)

Result:
no goals

Proof state:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ MemLp (fun x => g x * g' x) 1 (μ.restrict A)

Tactic:
have : ∀ᵐ x ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖ := by
  filter_upwards [ae_restrict_mem hA] with x hx
  refine (norm_mul_le _ _).trans ?_
  gcongr
  exact hC x (hAK hx)

Result:
case intro
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
this : ∀ᵐ (x : X) ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖
⊢ MemLp (fun x => g x * g' x) 1 (μ.restrict A)

Proof state:
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ ∀ᵐ (x : X) ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖

Tactic:
filter_upwards [ae_restrict_mem hA] with x hx

Result:
case h
X : Type u_1
R : Type u_5
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : MemLp g' 1 (μ.restrict A)
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
x : X
hx : x ∈ A
⊢ ‖g x * g' x‖ ≤ C * ‖g' x‖