awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Measurable (β := ℝ) fun (t : ℝ) ↦ μ.real {a : α | t < f a}
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : α | t < f a})
    (Measure.restrict volume (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable (β := ℝ) fun (t : ℝ) ↦ μ.real {a : α | t < f a}

Tactic:
Measurable.ennreal_toReal ?_

Premises used: MeasureTheory.Measure.real, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
⊢ Measurable (β := ℝ) fun (t : ℝ) ↦ μ.real {a : α | t < f a}

Tactic:
refine Measurable.ennreal_toReal ?_

Premises used: Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}

Tactic:
Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

Premises used: lt_of_le_of_lt, Antitone.measurable, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}

Tactic:
exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

Premises used: lt_of_le_of_lt, Antitone.measurable, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})

Tactic:
rw [Integrable.integral_eq_integral_meas_lt f_intble f_nn]

Premises used: MeasureTheory.Integrable.integral_eq_integral_meas_lt
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
h :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (a : ℝ) ↦ μ.real {a_1 : α | a < f a_1}) fun (a : ℝ) ↦ μ.real {a_1 : α | a ≤ f a_1}
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
h :
  ∀ (t : ℝ)
    (ht :
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)),
    μ.real {a : α | t < f a} = μ.real {a : α | t ≤ f a}
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (a : ℝ) ↦ μ.real {a_1 : α | a < f a_1}) fun (a : ℝ) ↦ μ.real {a_1 : α | a ≤ f a_1}

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht

Premises used: Set.Ioi, MeasureTheory.meas_le_ae_eq_meas_lt, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
t : ℝ
ht :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
⊢ μ.real {a : α | t < f a} = μ.real {a : α | t ≤ f a}

Tactic:
congrArg ENNReal.toReal ht.symm

Premises used: congrArg, MeasureTheory.Measure.real, ENNReal.toReal, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
t : ℝ
ht :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
⊢ μ.real {a : α | t < f a} = μ.real {a : α | t ≤ f a}

Tactic:
exact congrArg ENNReal.toReal ht.symm

Premises used: congrArg, ENNReal.toReal, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})

Tactic:
rw [f_intble.integral_eq_integral_meas_le f_nn]

Premises used: MeasureTheory.Integrable.integral_eq_integral_meas_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
rw : ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → μ.real {a : α | x ≤ f a} = 0
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})

Tactic:
rw [setIntegral_eq_of_subset_of_ae_diff_eq_zero
      nullMeasurableSet_Ioi Ioc_subset_Ioi_self ?_]

Premises used: nullMeasurableSet_Ioi, Set.Ioc_subset_Ioi_self, MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
apply : ∀ (t : ℝ) (ht : t ∈ Ioi 0 \ Ioc 0 M), μ.real {a : α | t ≤ f a} = 0
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → μ.real {a : α | x ≤ f a} = 0

Tactic:
apply Eventually.of_forall (fun t ht ↦ ?_)

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ M < t

Tactic:
simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]

Premises used: not_le, Set.mem_Ioi, Set.mem_diff, Set.mem_Ioc, not_and
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ M < t

Tactic:
have htM : M < t := by simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
rw : ∀ᵐ (a : α) ∂μ, a ∉ {a : α | M < f a}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_eq_zero_iff_ae_notMem]

Premises used: MeasureTheory.measure_eq_zero_iff_ae_notMem
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
a : α
ha : f a ≤ M
⊢ ¬M < f a

Tactic:
not_lt.mpr ha

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ (fun (x : α) ↦ M) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∉ {a : α | M < f a}) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : f a ≤ M), ¬M < f a
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a : α | M < f a}

Tactic:
filter_upwards [f_bdd] with a ha using not_lt.mpr ha
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have obs : μ {a | M < f a} = 0 := by
    rw [measure_eq_zero_iff_ae_notMem]
    filter_upwards [f_bdd] with a ha using not_lt.mpr ha
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real {a : α | t ≤ f a} = 0

Tactic:
rw [measureReal_def, ENNReal.toReal_eq_zero_iff]

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Or.inl <| measure_mono_null (fun a ha ↦ lt_of_lt_of_le htM ha) obs

Premises used: MeasureTheory.measure_mono_null, Or.inl, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact Or.inl <| measure_mono_null (fun a ha ↦ lt_of_lt_of_le htM ha) obs

Premises used: MeasureTheory.measure_mono_null, Or.inl, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
set :
  let F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a;
  lintegral μ F = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
set F := fun a : α => ⨆ n, f n a

Premises used: iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ lintegral μ F = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
le_antisymm ?_ (iSup_lintegral_le _)

Premises used: le_antisymm, MeasureTheory.iSup_lintegral_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
refine : lintegral μ F ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ lintegral μ F = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
refine le_antisymm ?_ (iSup_lintegral_le _)

Premises used: le_antisymm, MeasureTheory.iSup_lintegral_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
rw :
  LE.le (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
⊢ lintegral μ F ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_eq_nnreal]

Premises used: MeasureTheory.lintegral_eq_nnreal
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
iSup_le fun s => iSup_le fun hsf => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
refine :
  ∀ (s : α →ₛ ℝ≥0) (hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x),
    (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
refine iSup_le fun s => iSup_le fun hsf => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
⊢ (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
ENNReal.le_of_forall_lt_one_mul_le fun a ha => ?_

Premises used: ENNReal.le_of_forall_lt_one_mul_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
refine : ∀ (a : ℝ≥0∞) (ha : a < 1), a * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
refine ENNReal.le_of_forall_lt_one_mul_le fun a ha => ?_

Premises used: ENNReal.le_of_forall_lt_one_mul_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
a : ℝ≥0∞
ha : a < 1
rcases :
  ∀ (r : ℝ≥0),
    (↑r : ℝ≥0∞) < 1 →
      ∀ (ha : (↑r : ℝ≥0∞) < 1), (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ a * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 ha with ⟨r, rfl, _⟩

Premises used: ENNReal.lt_iff_exists_coe, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha : (↑r : ℝ≥0∞) < 1
⊢ r < 1

Tactic:
have ha : r < 1 := ENNReal.coe_lt_coe.1 ha
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
⊢ SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s

Tactic:
have eq_rs : rs.map c = (const α r : α →ₛ ℝ≥0∞) * map c s := rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
rw :
  Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})

Tactic:
rw [← inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
nth_rw :
  Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ univ)
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})

Tactic:
nth_rw 1 [← inter_univ (map c rs ⁻¹' {p})]

Premises used: Set.inter_univ, Set.preimage, Singleton.singleton, DFunLike.coe, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ univ)
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})

Tactic:
Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_

Premises used: Iff.mpr, Set.ext, setOf, true_iff, Membership.mem, LE.le, and_congr_right, Set.iUnion, iff_of_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
refine :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p}) x),
    Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ univ)
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})

Tactic:
refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_

Premises used: Iff.mpr, Set.ext, true_iff, and_congr_right, iff_of_eq