α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ 0 ≤ᵐ[μ] f
simp_rw [EventuallyLE, Pi.zero_apply]
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ (b : ℝ), b < 0 → ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x
rw [ae_const_le_iff_forall_lt_measure_zero]
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
⊢ ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ (b : ℝ), b < 0 → ↑↑μ {x | f x ≤ b} = 0
intro b hb_neg
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
⊢ ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
⊢ ↑↑μ {x | f x ≤ b} = 0
let s := {x | f x ≤ b}
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
⊢ ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
⊢ ↑↑μ {x | f x ≤ b} = 0
have hs : MeasurableSet s := hfm.measurableSet_le stronglyMeasurable_const
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
⊢ ↑↑μ {x | f x ≤ b} = 0
have mus : μ s < ∞ := by
  let c : ℝ≥0 := ⟨|b|, abs_nonneg _⟩
  have c_pos : (c : ℝ≥0∞) ≠ 0 := by simpa [← NNReal.coe_eq_zero] using hb_neg.ne
  calc
    μ s ≤ μ {x | (c : ℝ≥0∞) ≤ ‖f x‖₊} := by
      apply measure_mono
      intro x hx
      simp only [Set.mem_setOf_eq] at hx
      simpa only [nnnorm, abs_of_neg hb_neg, abs_of_neg (hx.trans_lt hb_neg), Real.norm_eq_abs,
        Subtype.mk_le_mk, neg_le_neg_iff, Set.mem_setOf_eq, ENNReal.coe_le_coe, NNReal] using hx
    _ ≤ (∫⁻ x, ‖f x‖₊ ∂μ) / c :=
      (meas_ge_le_lintegral_div hfm.aemeasurable.ennnorm c_pos ENNReal.coe_ne_top)
    _ < ∞ := ENNReal.div_lt_top (ne_of_lt hf.2) c_pos
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
⊢ ↑↑μ {x | f x ≤ b} = 0
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ ↑↑μ {x | f x ≤ b} = 0
have h_int_gt : (∫ x in s, f x ∂μ) ≤ b * (μ s).toReal := by
  have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
    refine'
      set_integral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) _
    rw [EventuallyLE, ae_restrict_iff hs]
    exact eventually_of_forall fun x hxs => hxs
  rwa [set_integral_const, smul_eq_mul, mul_comm] at h_const_le
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ False
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
⊢ ↑↑μ {x | f x ≤ b} = 0
by_contra h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ b * ENNReal.toReal (↑↑μ s) < ∫ (x : α) in s, f x ∂μ
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ False
refine' (lt_self_iff_false (∫ x in s, f x ∂μ)).mp (h_int_gt.trans_lt _)
case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 < ENNReal.toReal (↑↑μ s)

case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ b * ENNReal.toReal (↑↑μ s) < ∫ (x : α) in s, f x ∂μ
refine' (mul_neg_iff.mpr (Or.inr ⟨hb_neg, _⟩)).trans_le _
case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ

case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 < ENNReal.toReal (↑↑μ s)
case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 < ENNReal.toReal (↑↑μ s)

case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
swap
case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
⊢ ↑↑μ {x | f x ≤ b} = 0
case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 < ENNReal.toReal (↑↑μ s)
refine' ENNReal.toReal_nonneg.lt_of_ne fun h_eq => h _
case refine'_1.inl
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
hμs_eq_zero : ↑↑μ s = 0
⊢ ↑↑μ {x | f x ≤ b} = 0

case refine'_1.inr
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
hμs_eq_top : ↑↑μ s = ⊤
⊢ ↑↑μ {x | f x ≤ b} = 0
case refine'_1
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
⊢ ↑↑μ {x | f x ≤ b} = 0
cases' (ENNReal.toReal_eq_zero_iff _).mp h_eq.symm with hμs_eq_zero hμs_eq_top
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
⊢ ↑↑μ s < ⊤
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤
let c : ℝ≥0 := ⟨|b|, abs_nonneg _⟩
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
⊢ ↑↑μ s < ⊤
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
⊢ ↑↑μ s < ⊤
have c_pos : (c : ℝ≥0∞) ≠ 0 := by simpa [← NNReal.coe_eq_zero] using hb_neg.ne
no goals
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
⊢ ↑↑μ s < ⊤
calc
  μ s ≤ μ {x | (c : ℝ≥0∞) ≤ ‖f x‖₊} := by
    apply measure_mono
    intro x hx
    simp only [Set.mem_setOf_eq] at hx
    simpa only [nnnorm, abs_of_neg hb_neg, abs_of_neg (hx.trans_lt hb_neg), Real.norm_eq_abs,
      Subtype.mk_le_mk, neg_le_neg_iff, Set.mem_setOf_eq, ENNReal.coe_le_coe, NNReal] using hx
  _ ≤ (∫⁻ x, ‖f x‖₊ ∂μ) / c :=
    (meas_ge_le_lintegral_div hfm.aemeasurable.ennnorm c_pos ENNReal.coe_ne_top)
  _ < ∞ := ENNReal.div_lt_top (ne_of_lt hf.2) c_pos
no goals
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
⊢ ↑c ≠ 0
simpa [← NNReal.coe_eq_zero] using hb_neg.ne
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
⊢ s ⊆ {x | ↑c ≤ ↑‖f x‖₊}
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
⊢ ↑↑μ s ≤ ↑↑μ {x | ↑c ≤ ↑‖f x‖₊}
apply measure_mono
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
x : α
hx : x ∈ s
⊢ x ∈ {x | ↑c ≤ ↑‖f x‖₊}
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
⊢ s ⊆ {x | ↑c ≤ ↑‖f x‖₊}
intro x hx
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
x : α
hx : f x ≤ b
⊢ x ∈ {x | ↑c ≤ ↑‖f x‖₊}
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
x : α
hx : x ∈ s
⊢ x ∈ {x | ↑c ≤ ↑‖f x‖₊}
simp only [Set.mem_setOf_eq] at hx
no goals
case h
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
c : ℝ≥0 := { val := abs b, property := (_ : 0 ≤ abs b) }
c_pos : ↑c ≠ 0
x : α
hx : f x ≤ b
⊢ x ∈ {x | ↑c ≤ ↑‖f x‖₊}
simpa only [nnnorm, abs_of_neg hb_neg, abs_of_neg (hx.trans_lt hb_neg), Real.norm_eq_abs,
  Subtype.mk_le_mk, neg_le_neg_iff, Set.mem_setOf_eq, ENNReal.coe_le_coe, NNReal] using hx
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_const_le : (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, b ∂μ
⊢ (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
  refine'
    set_integral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) _
  rw [EventuallyLE, ae_restrict_iff hs]
  exact eventually_of_forall fun x hxs => hxs
no goals
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_const_le : (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, b ∂μ
⊢ (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
rwa [set_integral_const, smul_eq_mul, mul_comm] at h_const_le
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ (fun x => f x) ≤ᵐ[Measure.restrict μ s] fun x => b
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, b ∂μ
refine'
  set_integral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) _
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ (fun x => f x) ≤ᵐ[Measure.restrict μ s] fun x => b
rw [EventuallyLE, ae_restrict_iff hs]
no goals
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b
exact eventually_of_forall fun x hxs => hxs
case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in {x | f x ≤ b}, f x ∂μ
case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
simp_rw [Measure.restrict_restrict hs]
no goals
case refine'_2
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
⊢ 0 ≤ ∫ (x : α) in {x | f x ≤ b}, f x ∂μ
exact hf_zero s hs mus
no goals
case refine'_1.inl
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
hμs_eq_zero : ↑↑μ s = 0
⊢ ↑↑μ {x | f x ≤ b} = 0
exact hμs_eq_zero
no goals
case refine'_1.inr
α : Type u_1
E : Type ?u.69084
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hfm : StronglyMeasurable f
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : MeasurableSet s
mus : ↑↑μ s < ⊤
h_int_gt : (∫ (x : α) in s, f x ∂μ) ≤ b * ENNReal.toReal (↑↑μ s)
h : ¬↑↑μ {x | f x ≤ b} = 0
h_eq : 0 = ENNReal.toReal (↑↑μ s)
hμs_eq_top : ↑↑μ s = ⊤
⊢ ↑↑μ {x | f x ≤ b} = 0
exact absurd hμs_eq_top mus.ne