-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem MonotoneOn.memLp_top (hmono : MonotoneOn f s) {a b : X}
    (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) :
    MemLp f ∞ (μ.restrict s)

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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖

Tactic:
apply (ae_restrict_iff' h's).mpr

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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)

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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _

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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ MemLp f ⊤ (μ.restrict s)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
borelize E

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp f ⊤ (μ.restrict s)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩

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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
⊢ MemLp f ⊤ (μ.restrict s)