-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_gt_gt {R : ℝ} {f : X → ℝ} (hR : 0 ≤ R)
    (hfint : IntegrableOn f {x | ↑R < f x} μ) (hμ : μ {x | ↑R < f x} ≠ 0) :
    (μ {x | ↑R < f x}).toReal * R < ∫ x in {x | ↑R < f x}, f x ∂μ

Proof state:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 ≤ᶠ[ae (μ.restrict {x | R < f x})] fun a => f a - R

Tactic:
rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]

Result:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ ∀ᵐ (x : X) ∂μ, x ∈ {x | R < f x} → 0 ≤ f x - R

case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ ∫⁻ (a : X) in {x | R < f x}, ‖(fun x => R) a‖ₑ ∂μ ≤ ∫⁻ (a : X) in {x | R < f x}, ‖f a‖ₑ ∂μ

Tactic:
refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
x : X
hx : x ∈ {x | R < f x}
⊢ ‖(fun x => R) x‖ₑ ≤ ‖f x‖ₑ

Proof state:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})

Tactic:
exact nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ (μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ

Tactic:
have : IntegrableOn (fun _ => R) {x | ↑R < f x} μ := by
  refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
  refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
  simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
    Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx), Subtype.mk_le_mk]
  exact le_of_lt hx

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ (μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ IntegrableOn (fun x => R) {x | R < f x} μ

Tactic:
refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ ∫⁻ (a : X) in {x | R < f x}, ‖(fun x => R) a‖ₑ ∂μ ≤ ∫⁻ (a : X) in {x | R < f x}, ‖f a‖ₑ ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
x : X
hx : x ∈ {x | R < f x}
⊢ ⟨R, hR⟩ ≤ ⟨f x, ⋯⟩

Tactic:
exact le_of_lt hx

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : 0 < μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ {x | R < f x} ⊆ support fun a => f a - R

Tactic:
exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)

Result:
no goals

Proof state:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ ∀ᵐ (x : X) ∂μ, x ∈ {x | R < f x} → 0 ≤ f x - R

Tactic:
exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx

Result:
no goals

Proof state:
case hfi
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ IntegrableOn (fun a => f a - R) {x | R < f x} μ

Tactic:
exact Integrable.sub hfint this

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : 0 < μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 < μ ((support fun a => f a - R) ∩ {x | R < f x})

Tactic:
rwa [Set.inter_eq_self_of_subset_right]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : 0 < μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ {x | R < f x} ⊆ support fun a => f a - R

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 < μ ((support fun a => f a - R) ∩ {x | R < f x})

Tactic:
rw [← zero_lt_iff] at hμ

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : 0 < μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 < μ ((support fun a => f a - R) ∩ {x | R < f x})

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ (μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ

Tactic:
rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
  setIntegral_pos_iff_support_of_nonneg_ae]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 < μ ((support fun a => f a - R) ∩ {x | R < f x})

case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ 0 ≤ᶠ[ae (μ.restrict {x | R < f x})] fun a => f a - R

case hfi
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x} μ
⊢ IntegrableOn (fun a => f a - R) {x | R < f x} μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
x : X
hx : x ∈ {x | R < f x}
⊢ ‖(fun x => R) x‖ₑ ≤ ‖f x‖ₑ

Tactic:
simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
  Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx), Subtype.mk_le_mk]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
x : X
hx : x ∈ {x | R < f x}
⊢ ⟨R, hR⟩ ≤ ⟨f x, ⋯⟩