-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_trim {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
    ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ

Proof state:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g

Result:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Proof state:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ

Tactic:
rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]

Result:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun x => c)

Tactic:
intro c s hs

Result:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ

Proof state:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
            (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
              (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)

Tactic:
intro f g _ hf _ hf_prop hg_prop

Result:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : (μ.trim hm) s = μ s
⊢ c * (μ.trim hm) s = c * μ s

Tactic:
rw [h_trim_s]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)) →
          (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) fun x => ⨆ n, f n x

Tactic:
intro f hf hf_mono hf_prop

Result:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ

Proof state:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g

Result:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Proof state:
case refine_2
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
rwa [hf_prop, hg_prop, ← h_m0] at h_m

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ

Tactic:
rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const,
  setLIntegral_const]

Result:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * (μ.trim hm) s = c * μ s

Proof state:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ

Tactic:
rw [lintegral_iSup hf hf_mono]

Result:
case refine_3
α : Type u_1
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 ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun x => ⨆ n, f n x) a ∂μ