-- Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean
theorem limsup_trim (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
    limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
suffices h_meas_eq : μ { x | ¬f x ≤ a } = μ.trim hm { x | ¬f x ≤ a } by
  simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}
⊢ a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
ext1 a

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
h_set_eq : {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}
⊢ sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
rw [h_set_eq]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
simp_rw [limsup_eq]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Measurable fun x => a

Tactic:
exact @measurable_const _ _ _ m _

Result:
no goals

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}

Tactic:
refine (trim_measurableSet_eq hm ?_).symm

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet {x | ¬f x ≤ a}

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet {x | ¬f x ≤ a}

Tactic:
refine @MeasurableSet.compl _ _ m (@measurableSet_le ℝ≥0∞ _ _ _ _ m _ _ _ _ _ hf ?_)

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Measurable fun x => a

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
suffices h_set_eq : { a : ℝ≥0∞ | ∀ᵐ n ∂μ.trim hm, f n ≤ a } = { a : ℝ≥0∞ | ∀ᵐ n ∂μ, f n ≤ a } by
  rw [h_set_eq]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}