awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator 1 a ∂μ = ∫⁻ (a : α), s.indicator 1 a ∂ν

Tactic:
exact h (s.indicator 1) ((measurable_indicator_const_iff 1).mpr hs)

Premises used: Iff.mpr, Set.indicator, measurable_indicator_const_iff, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
⊢ μ = ν

Tactic:
(μ.ext_iff_lintegral ν).mpr hμν

Premises used: Iff.mpr, MeasureTheory.Measure.ext_iff_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
hm : ∀ (i : β), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
simp only [Measure.restrict_iUnion_ae hd hm, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.restrict_iUnion_ae, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
hm : ∀ (i : β), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
lintegral_iUnion₀ (fun i => (hm i).nullMeasurableSet) hd.aedisjoint f

Premises used: MeasureTheory.lintegral_iUnion₀, MeasurableSet.nullMeasurableSet, Pairwise.aedisjoint
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
haveI :
  ∀ (this : Encodable (↑t : Type u_2)),
    ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ

Tactic:
haveI := ht.toEncodable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable (↑t : Type u_2)
rw :
  ∫⁻ (a : α) in ⋃ (x : (↑t : Type u_2)), s (↑x : β), f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ)
    (∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ)
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ

Tactic:
rw [biUnion_eq_iUnion, lintegral_iUnion₀ (SetCoe.forall'.1 hm) (hd.subtype _ _)]

Premises used: MeasureTheory.lintegral_iUnion₀, Set.Pairwise.subtype, Iff.mp, Set.biUnion_eq_iUnion, SetCoe.forall'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, MeasurableSet (s i)
hd : t.PairwiseDisjoint s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ

Tactic:
lintegral_biUnion₀ ht (fun i hi => (hm i hi).nullMeasurableSet) hd.aedisjoint f

Premises used: MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint, MeasureTheory.lintegral_biUnion₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
t : β → Set α
hd : (↑s : Set β).Pairwise (AEDisjoint μ on t)
hm : ∀ b ∈ s, NullMeasurableSet (t b) μ
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

Tactic:
simp only [← Finset.mem_coe, lintegral_biUnion₀ s.countable_toSet hm hd, ← Finset.tsum_subtype']

Premises used: Finset.countable_toSet, MeasureTheory.lintegral_biUnion₀, Finset.mem_coe, Finset.tsum_subtype'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
t : β → Set α
hd : (↑s : Set β).PairwiseDisjoint t
hm : ∀ b ∈ s, MeasurableSet (t b)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

Tactic:
lintegral_biUnion_finset₀ hd.aedisjoint (fun b hb => (hm b hb).nullMeasurableSet) f

Premises used: MeasureTheory.lintegral_biUnion_finset₀, MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
f : α → ℝ≥0∞
rw : ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun (i : β) ↦ μ.restrict (s i)
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
rw [← lintegral_sum_measure]

Premises used: MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun (i : β) ↦ μ.restrict (s i)

Tactic:
lintegral_mono' restrict_iUnion_le le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_iUnion_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun (i : β) ↦ μ.restrict (s i)

Tactic:
exact lintegral_mono' restrict_iUnion_le le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_iUnion_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A B : Set α
hB : MeasurableSet B
hAB : Disjoint A B
rw : ∫⁻ (a : α), f a ∂(μ.restrict A + μ.restrict B) = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
⊢ ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ

Tactic:
rw [restrict_union hAB hB, lintegral_add_measure]

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.Measure.restrict_union
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
rw : ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ

Tactic:
rw [← lintegral_add_measure]

Premises used: MeasureTheory.lintegral_add_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)

Tactic:
lintegral_mono' (restrict_union_le _ _) le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_union_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)

Tactic:
exact lintegral_mono' (restrict_union_le _ _) le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_union_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
rw : ∫⁻ (a : α), f a ∂(μ.restrict (A ∩ B) + μ.restrict (A \ B)) = ∫⁻ (x : α) in A, f x ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in A, f a ∂μ = ∫⁻ (x : α) in A, f x ∂μ
⊢ ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ

Tactic:
rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.Measure.restrict_inter_add_diff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A : Set α
hA : MeasurableSet A
rw : ∫⁻ (a : α), f a ∂(μ.restrict A + μ.restrict Aᶜ) = ∫⁻ (x : α), f x ∂μ
rw₁ rw₂ : ∫⁻ (a : α), f a ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.Measure.restrict_add_restrict_compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
rw :
  ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ +
      ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ =
    ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ
⊢ ∫⁻ (a : α), s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

Tactic:
rw [← lintegral_add_compl _ hs]

Premises used: MeasureTheory.lintegral_add_compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
e_a : ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in s, f a ∂μ
e_a₁ : ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in sᶜ, g a ∂μ
⊢ ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ +
      ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ =
    ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
setLIntegral_congr_fun hs <| fun _ ↦ Set.piecewise_eq_of_mem _ _ _

Premises used: MeasureTheory.setLIntegral_congr_fun, Set.piecewise_eq_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
exact setLIntegral_congr_fun hs <| fun _ ↦ Set.piecewise_eq_of_mem _ _ _

Premises used: MeasureTheory.setLIntegral_congr_fun, Set.piecewise_eq_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in sᶜ, g a ∂μ

Tactic:
setLIntegral_congr_fun hs.compl <| fun _ ↦ Set.piecewise_eq_of_notMem _ _ _

Premises used: Set.piecewise_eq_of_notMem, MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in sᶜ, g a ∂μ

Tactic:
exact setLIntegral_congr_fun hs.compl <| fun _ ↦ Set.piecewise_eq_of_notMem _ _ _

Premises used: Set.piecewise_eq_of_notMem, MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
rw : ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ + ∫⁻ (x : α) in sᶜ, f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
rw₁ rw₂ : ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in sᶜ, f x ∂μ
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← lintegral_add_compl (μ := μ) f hsm, ENNReal.add_sub_cancel_left hfs]

Premises used: ENNReal.add_sub_cancel_left, MeasureTheory.lintegral_add_compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst : Countable ι
f : α → ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ ∫⁻ (x : α) in ⋃ (i : ι), s i, f x ∂μ = ⨆ (i : ι), ∫⁻ (x : α) in s i, f x ∂μ

Tactic:
simp only [lintegral_def, iSup_comm (ι := ι),
    SimpleFunc.lintegral_restrict_iUnion_of_directed _ hd]

Premises used: MeasureTheory.lintegral_def, iSup_comm, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}

Tactic:
have hm : MeasurableSet { x | f x ≤ g x } := measurableSet_le hf hg
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
rw :
  ∫⁻ (x : α) in {x : α | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x : α | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x ∂μ
⊢ ∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x ∂μ

Tactic:
rw [← lintegral_add_compl (fun x => max (f x) (g x)) hm]

Premises used: MeasureTheory.lintegral_add_compl, Max.max
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
simp :
  ∫⁻ (x : α) in {x : α | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x : α | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a : α | f a ≤ g a}ᶜ, f x ∂μ
⊢ ∫⁻ (x : α) in {x : α | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x : α | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x ∂μ

Tactic:
simp only [← compl_setOf, ← not_le]

Premises used: not_le, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x : α | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x : α | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a : α | f a ≤ g a}ᶜ, f x ∂μ

Tactic:
congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl, HAdd.hAdd, congr_arg₂
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
refine_1 : EqOn (fun (x : α) ↦ max (f x) (g x)) g {x : α | f x ≤ g x}
refine_2 : EqOn (fun (x : α) ↦ max (f x) (g x)) f {x : α | f x ≤ g x}ᶜ
⊢ ∫⁻ (x : α) in {x : α | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x : α | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a : α | f a ≤ g a}ᶜ, f x ∂μ

Tactic:
refine congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl, HAdd.hAdd, congr_arg₂
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
⊢ EqOn (fun (x : α) ↦ max (f x) (g x)) g {x : α | f x ≤ g x}

Tactic:
fun x => max_eq_right (a := f x) (b := g x)

Premises used: Set.Mem, setOf, Set.EqOn, max_eq_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
⊢ EqOn (fun (x : α) ↦ max (f x) (g x)) f {x : α | f x ≤ g x}ᶜ

Tactic:
fun x (hx : ¬ f x ≤ g x) => max_eq_left (not_le.1 hx).le

Premises used: not_le, Set.Mem, setOf, LT.lt.le, max_eq_left, Set.EqOn, Iff.mp, Not
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
⊢ EqOn (fun (x : α) ↦ max (f x) (g x)) g {x : α | f x ≤ g x}

Tactic:
exacts [fun x => max_eq_right (a := f x) (b := g x),
    fun x (hx : ¬ f x ≤ g x) => max_eq_left (not_le.1 hx).le]

Premises used: not_le, LT.lt.le, max_eq_left, max_eq_right, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
rw : MeasurableSet.{u_1} (α := α) {x : α | g x < f x}
rw₁ : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
⊢ ∫⁻ (x : α) in s, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in s ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x : α | g x < f x}, f x ∂μ

Tactic:
rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]

Premises used: MeasureTheory.Measure.restrict_restrict, Set.inter_comm, MeasureTheory.lintegral_max
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet.{u_1} (α := α) {x : α | g x < f x}

Tactic:
measurableSet_lt hg hf

Premises used: setOf, measurableSet_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}

Tactic:
measurableSet_le hf hg

Premises used: measurableSet_le, setOf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet.{u_1} (α := α) {x : α | g x < f x}

Tactic:
exacts [measurableSet_lt hg hf, measurableSet_le hf hg]

Premises used: measurableSet_le, measurableSet_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → ℝ≥0∞
hbdd : ∃ (y : ℝ≥0), ∀ x ∈ s, f x ≤ (↑y : ℝ≥0∞)
obtain : ∀ (M : ℝ≥0) (hM : ∀ x ∈ s, f x ≤ (↑M : ℝ≥0∞)), ∫⁻ (x : α) in s, f x ∂μ < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞

Tactic:
obtain ⟨M, hM⟩ := hbdd
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ (↑M : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞

Tactic:
lt_of_le_of_lt (setLIntegral_mono measurable_const hM) ?_

Premises used: lt_of_le_of_lt, MeasureTheory.setLIntegral_mono, measurable_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ (↑M : ℝ≥0∞)
refine : ∫⁻ (x : α) in s, (↑M : ℝ≥0∞) ∂μ < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞

Tactic:
refine lt_of_le_of_lt (setLIntegral_mono measurable_const hM) ?_

Premises used: lt_of_le_of_lt, MeasureTheory.setLIntegral_mono, measurable_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ (↑M : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, (↑M : ℝ≥0∞) ∂μ < ∞

Tactic:
simp [ENNReal.mul_lt_top, hs.lt_top]

Premises used: ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → ℝ≥0
hbdd : BddAbove (f '' s)
⊢ ∫⁻ (x : α) in s, (↑(f x) : ℝ≥0∞) ∂μ < ∞

Tactic:
setLIntegral_lt_top_of_le_nnreal hs <| hbdd.imp fun _M hM _x hx ↦
    ENNReal.coe_le_coe.2 <| hM (mem_image_of_mem f hx)

Premises used: Iff.mpr, MeasureTheory.setLIntegral_lt_top_of_le_nnreal, ENNReal.coe_le_coe, Exists.imp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hsc : IsCompact s
f : α → ℝ≥0
hf : Continuous[inst, _] f
⊢ ∫⁻ (x : α) in s, (↑(f x) : ℝ≥0∞) ∂μ < ∞

Tactic:
setLIntegral_lt_top_of_bddAbove hs (hsc.image hf).bddAbove

Premises used: IsCompact.bddAbove, MeasureTheory.setLIntegral_lt_top_of_bddAbove, IsCompact.image
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
rw : HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
⊢ ∫⁻ (x : α) in s, c ∂μ < ∞

Tactic:
rw [lintegral_const]

Premises used: MeasureTheory.lintegral_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top hc.lt_top (measure_lt_top (μ.restrict s) univ)

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.Measure.restrict, ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top (μ.restrict s) univ)

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.Measure.restrict, ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ ∫⁻ (x : α), c ∂μ < ∞

Tactic:
simpa only [Measure.restrict_univ] using setLIntegral_const_lt_top (univ : Set α) hc

Premises used: Set.univ, MeasureTheory.setLIntegral_const_lt_top, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫⁻ (x : α), f x ∂μ = c

Tactic:
simp [lintegral_congr_ae hf]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≤ c
⊢ ∫⁻ (a : α), c ∂μ = c

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : α → ℝ≥0∞
⊢ ⨅ (x : α), f x ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : α → ℝ≥0∞
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ ⨆ (x : α), f x

Tactic:
simp