-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_restrict_iUnion_of_directed {ι : Type*} [Countable ι]
    (f : α →ₛ ℝ≥0∞) {s : ι → Set α} (hd : Directed (· ⊆ ·) s) (μ : Measure α) :
    f.lintegral (μ.restrict (⋃ i, s i)) = ⨆ i, f.lintegral (μ.restrict (s i))

Proof state:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
⊢ ∑ x ∈ f.range, ⨆ i, x * (μ.restrict (s i)) (⇑f ⁻¹' {x}) = ⨆ i, ∑ x ∈ f.range, x * (μ.restrict (s i)) (⇑f ⁻¹' {x})

Tactic:
refine finsetSum_iSup fun i j ↦ (hd i j).imp fun k ⟨hik, hjk⟩ ↦ fun a ↦ ?_

Result:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s i)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a}) ∧
    a * (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

Proof state:
case right
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

Tactic:
gcongr

Result:
case right.bc
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ (μ.restrict (s k)) (⇑f ⁻¹' {a})

Proof state:
case right.bc
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ (μ.restrict (s k)) (⇑f ⁻¹' {a})

Tactic:
refine Measure.restrict_mono ?_ le_rfl _

Result:
case right.bc
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ s j ⊆ s k

Proof state:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
⊢ f.lintegral (μ.restrict (⋃ i, s i)) = ⨆ i, f.lintegral (μ.restrict (s i))

Tactic:
simp only [lintegral, Measure.restrict_iUnion_apply_eq_iSup hd (measurableSet_preimage ..),
  ENNReal.mul_iSup]

Result:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
⊢ ∑ x ∈ f.range, ⨆ i, x * (μ.restrict (s i)) (⇑f ⁻¹' {x}) = ⨆ i, ∑ x ∈ f.range, x * (μ.restrict (s i)) (⇑f ⁻¹' {x})

Proof state:
case right.bc
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 => x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 => x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 => x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ s j ⊆ s k

Tactic:
assumption

Result:
no goals