case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
⊢ f =ᵐ[μ] 0
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
⊢ f =ᵐ[μ] 0
obtain ⟨t, ht_meas, htf_zero, htμ⟩ := hf.exists_set_sigmaFinite
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
⊢ f =ᵐ[μ] 0
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
⊢ f =ᵐ[μ] 0
haveI : SigmaFinite ((μ.restrict t).trim hm) := by rwa [restrict_trim hm μ ht_meas] at htμ
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
⊢ f =ᵐ[μ] 0
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
⊢ f =ᵐ[μ] 0
have htf_zero : f =ᵐ[μ.restrict (tᶜ)] 0 := by
  rw [EventuallyEq, ae_restrict_iff' (MeasurableSet.compl (hm _ ht_meas))]
  exact eventually_of_forall htf_zero
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[μ] 0
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
⊢ f =ᵐ[μ] 0
have hf_meas_m : StronglyMeasurable[m] f := hf.stronglyMeasurable
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this✝ : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
this : f =ᵐ[Measure.restrict μ t] 0
⊢ f =ᵐ[μ] 0

case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[Measure.restrict μ t] 0
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[μ] 0
suffices : f =ᵐ[μ.restrict t] 0
case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[Measure.restrict μ t] 0
case intro.intro.intro
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this✝ : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
this : f =ᵐ[Measure.restrict μ t] 0
⊢ f =ᵐ[μ] 0

case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[Measure.restrict μ t] 0
exact ae_of_ae_restrict_of_ae_restrict_compl _ this htf_zero
case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ↑↑(Measure.trim (Measure.restrict μ t) hm) ({x | (fun x => f x = OfNat.ofNat 0 x) x}ᶜ) = 0
case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ f =ᵐ[Measure.restrict μ t] 0
refine' measure_eq_zero_of_trim_eq_zero hm _
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤ → IntegrableOn (fun x => f x) s

case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤ →
        (∫ (x : α) in s, f x ∂Measure.trim (Measure.restrict μ t) hm) = 0
case this
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ↑↑(Measure.trim (Measure.restrict μ t) hm) ({x | (fun x => f x = OfNat.ofNat 0 x) x}ᶜ) = 0
refine' ae_eq_zero_of_forall_set_integral_eq_of_sigmaFinite _ _
no goals
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
⊢ SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
rwa [restrict_trim hm μ ht_meas] at htμ
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → f x = OfNat.ofNat 0 x
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
⊢ f =ᵐ[Measure.restrict μ (tᶜ)] 0
rw [EventuallyEq, ae_restrict_iff' (MeasurableSet.compl (hm _ ht_meas))]
no goals
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → f x = OfNat.ofNat 0 x
exact eventually_of_forall htf_zero
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ IntegrableOn (fun x => f x) s
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤ → IntegrableOn (fun x => f x) s
intro s hs hμs
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ Integrable fun x => f x
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ IntegrableOn (fun x => f x) s
unfold IntegrableOn
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ Integrable fun x => f x
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ Integrable fun x => f x
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ Integrable fun x => f x
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ Integrable fun x => f x
rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs,
  trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ Integrable fun x => f x
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ Integrable fun x => f x
refine' Integrable.trim hm _ hf_meas_m
no goals
case this.refine'_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ Integrable fun x => f x
exact hf_int_finite _ (hs.inter ht_meas) hμs
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ (∫ (x : α) in s, f x ∂Measure.trim (Measure.restrict μ t) hm) = 0
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤ →
        (∫ (x : α) in s, f x ∂Measure.trim (Measure.restrict μ t) hm) = 0
intro s hs hμs
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ (∫ (x : α), f x ∂Measure.trim (Measure.restrict μ (s ∩ t)) hm) = 0
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ (∫ (x : α) in s, f x ∂Measure.trim (Measure.restrict μ t) hm) = 0
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ (∫ (x : α), f x ∂Measure.trim (Measure.restrict μ (s ∩ t)) hm) = 0
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim (Measure.restrict μ t) hm) s < ⊤
⊢ (∫ (x : α), f x ∂Measure.trim (Measure.restrict μ (s ∩ t)) hm) = 0
rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs,
  trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ (∫ (x : α) in s ∩ t, f x ∂μ) = 0
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ (∫ (x : α), f x ∂Measure.trim (Measure.restrict μ (s ∩ t)) hm) = 0
rw [← integral_trim hm hf_meas_m]
no goals
case this.refine'_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf : FinStronglyMeasurable f (Measure.trim μ hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict (Measure.trim μ hm) t)
this : SigmaFinite (Measure.trim (Measure.restrict μ t) hm)
htf_zero : f =ᵐ[Measure.restrict μ (tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ (s ∩ t) < ⊤
⊢ (∫ (x : α) in s ∩ t, f x ∂μ) = 0
exact hf_zero _ (hs.inter ht_meas) hμs