-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem ContinuousOn.integrableOn_compact'
    (hK : IsCompact K) (h'K : MeasurableSet K) (hf : ContinuousOn f K) :
    IntegrableOn f K μ

Proof state:
case intro
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict K)

Tactic:
apply hasFiniteIntegral_of_bounded (C := C)

Result:
case intro
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.restrict K, ‖f a‖ ≤ C

Proof state:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
⊢ HasFiniteIntegral f (μ.restrict K)

Tactic:
obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
  IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded

Result:
case intro
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict K)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
⊢ IntegrableOn f K μ

Tactic:
refine ⟨ContinuousOn.aestronglyMeasurable_of_isCompact hf hK h'K, ?_⟩

Result:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
⊢ HasFiniteIntegral f (μ.restrict K)

Proof state:
case intro
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.restrict K, ‖f a‖ ≤ C

Tactic:
filter_upwards [ae_restrict_mem h'K] with x hx using hC _ (mem_image_of_mem f hx)

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
⊢ HasFiniteIntegral f (μ.restrict K)

Tactic:
have : Fact (μ K < ∞) := ⟨hK.measure_lt_top⟩

Result:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : OpensMeasurableSpace X
K : Set X
inst✝ : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
this : Fact (μ K < ⊤)
⊢ HasFiniteIntegral f (μ.restrict K)