case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (indicator s fun x => c)

case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) f →
            (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) g →
              (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f + g)

case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)) →
          (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) fun x => ⨆ (n : ℕ), f n x
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
refine'
  @Measurable.ennreal_induction α m (fun f => (∫⁻ a, f a ∂μ.trim hm) = ∫⁻ a, f a ∂μ) _ _ _ f hf
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.trim μ hm) = ∫⁻ (a : α), indicator s (fun x => c) a ∂μ
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (indicator s fun x => c)
intro c s hs
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * ↑↑(Measure.trim μ hm) s = c * ↑↑μ s
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.trim μ hm) = ∫⁻ (a : α), indicator s (fun x => c) a ∂μ
rw [lintegral_indicator _ hs, lintegral_indicator _ (hm s hs), set_lintegral_const,
  set_lintegral_const]
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : ↑↑(Measure.trim μ hm) s = ↑↑μ s
⊢ c * ↑↑(Measure.trim μ hm) s = c * ↑↑μ s

case h_trim_s
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(Measure.trim μ hm) s = ↑↑μ s
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * ↑↑(Measure.trim μ hm) s = c * ↑↑μ s
suffices h_trim_s : μ.trim hm s = μ s
no goals
case h_trim_s
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(Measure.trim μ hm) s = ↑↑μ s
exact trim_measurableSet_eq hm hs
no goals
case refine'_1
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : ↑↑(Measure.trim μ hm) s = ↑↑μ s
⊢ c * ↑↑(Measure.trim μ hm) s = c * ↑↑μ s
rw [h_trim_s]
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) f →
            (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) g →
              (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f + g)
intro f g _ hf _ hf_prop hg_prop
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
h_m :
  (∫⁻ (a : α), f a + g a ∂Measure.trim μ hm) = (∫⁻ (a : α), f a ∂Measure.trim μ hm) + ∫⁻ (a : α), g a ∂Measure.trim μ hm
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
h_m :
  (∫⁻ (a : α), f a + g a ∂Measure.trim μ hm) = (∫⁻ (a : α), f a ∂Measure.trim μ hm) + ∫⁻ (a : α), g a ∂Measure.trim μ hm
h_m0 : (∫⁻ (a : α), f a + g a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
h_m :
  (∫⁻ (a : α), f a + g a ∂Measure.trim μ hm) = (∫⁻ (a : α), f a ∂Measure.trim μ hm) + ∫⁻ (a : α), g a ∂Measure.trim μ hm
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g
no goals
case refine'_2
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (support f) (support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
hg_prop : (∫⁻ (a : α), g a ∂Measure.trim μ hm) = ∫⁻ (a : α), g a ∂μ
h_m :
  (∫⁻ (a : α), f a + g a ∂Measure.trim μ hm) = (∫⁻ (a : α), f a ∂Measure.trim μ hm) + ∫⁻ (a : α), g a ∂Measure.trim μ hm
h_m0 : (∫⁻ (a : α), f a + g a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), (f + g) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (f + g) a ∂μ
rwa [hf_prop, hg_prop, ← h_m0] at h_m
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂μ
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)) →
          (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) fun x => ⨆ (n : ℕ), f n x
intro f hf hf_mono hf_prop
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = ∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂μ
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂Measure.trim μ hm) = ∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂μ
rw [lintegral_iSup hf hf_mono]
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = ∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f n x) a ∂μ
rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]
case refine'_3.e_s
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (fun n => ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = fun n => ∫⁻ (a : α), f n a ∂μ
case refine'_3
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
congr
no goals
case refine'_3.e_s
α : Type u_1
β : Type ?u.1822393
γ : Type ?u.1822396
δ : Type ?u.1822399
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun f => (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ (fun n => ∫⁻ (a : α), f n a ∂Measure.trim μ hm) = fun n => ∫⁻ (a : α), f n a ∂μ
exact funext fun n => hf_prop n