awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
⊢ ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) r ((μ.restrict {x : α | f x = r} : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
Tactic: rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
rw :
  HMul.hMul (β := ℝ≥0∞) r ((μ.restrict {x : α | f x = r} : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
⊢ ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ {x : α | f x = r}) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
Tactic: rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
rw :
  HMul.hMul (β := ℝ≥0∞) r ((μ.restrict {x : α | f x = r} : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ {x : α | f x = r}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
⊢ ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have rw₂ : HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
Tactic: rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ = ν
x : α → ℝ≥0∞
h_1 : Measurable x
⊢ ∫⁻ (a : α), x a ∂μ = ∫⁻ (a : α), x a ∂ν
have rw : ∫⁻ (a : α), x a ∂ν = ∫⁻ (a : α), x a ∂ν
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = ν ↔ ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
have refine : (∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν) → μ = ν
Tactic: refine ⟨fun h _ _ ↦ by rw [h], ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
⊢ μ = ν
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (a : α), s.indicator 1 a ∂μ = ∫⁻ (a : α), s.indicator 1 a ∂ν
Tactic: simp only [← lintegral_indicator_one hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ
have 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 ∂μ
Tactic: haveI := ht.toEncodable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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)
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ
have rw : ∫⁻ (a : α) in ⋃ (x : (↑t : Type u_2)), s (↑x : β), 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 _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : (↑t : Type u_2)), ∫⁻ (a : α) in s (↑i : β), f a ∂μ
have 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 ∂μ)
Tactic: rw [biUnion_eq_iUnion, lintegral_iUnion₀ (SetCoe.forall'.1 hm) (hd.subtype _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
have rw : ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun (i : β) ↦ μ.restrict (s i)
Tactic: rw [← lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A B : Set α
hB : MeasurableSet B
hAB : Disjoint A B
⊢ ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
have rw : ∫⁻ (a : α), f a ∂(μ.restrict A + μ.restrict B) = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
Tactic: rw [restrict_union hAB hB, lintegral_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
have rw₁ : ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
Tactic: rw [restrict_union hAB hB, lintegral_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ
have rw : ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)
Tactic: rw [← lintegral_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
⊢ ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
have rw : ∫⁻ (a : α), f a ∂(μ.restrict (A ∩ B) + μ.restrict (A \ B)) = ∫⁻ (x : α) in A, f x ∂μ
Tactic: rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
have rw₁ : ∫⁻ (a : α) in A, f a ∂μ = ∫⁻ (x : α) in A, f x ∂μ
Tactic: rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw : ∫⁻ (a : α), f a ∂(μ.restrict A + μ.restrict Aᶜ) = ∫⁻ (x : α), f x ∂μ
Tactic: rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw₁ : ∫⁻ (a : α), f a ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (a : α), s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ
have 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 ∂μ
Tactic: rw [← lintegral_add_compl _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ +
      ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ =
    ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ
have e_a : ∫⁻ (x : α) in s, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (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 ∂μ
have e_a₁ : ∫⁻ (x : α) in sᶜ, s.piecewise (β := fun (i : α) ↦ ℝ≥0∞) f g x ∂μ = ∫⁻ (a : α) in sᶜ, g a ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
have rw : ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ + ∫⁻ (x : α) in sᶜ, f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
Tactic: rw [← lintegral_add_compl (μ := μ) f hsm, ENNReal.add_sub_cancel_left hfs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
have rw₁ : ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in sᶜ, f x ∂μ
Tactic: rw [← lintegral_add_compl (μ := μ) f hsm, ENNReal.add_sub_cancel_left hfs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable 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 ∂μ
have hm : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
Tactic: have hm : MeasurableSet { x | f x ≤ g x } := measurableSet_le hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x ∂μ
have 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 ∂μ
Tactic: rw [← lintegral_add_compl (fun x => max (f x) (g x)) hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 {x : α | g x < f x}, f x ∂μ
have 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 ∂μ
Tactic: simp only [← compl_setOf, ← not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
have refine_1 : EqOn (fun (x : α) ↦ max (f x) (g x)) g {x : α | f x ≤ g x}
Tactic: refine congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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}
⊢ ∫⁻ (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 ∂μ
have refine_2 : EqOn (fun (x : α) ↦ max (f x) (g x)) f {x : α | f x ≤ g x}ᶜ
Tactic: refine congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ ∫⁻ (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 ∂μ
have rw : MeasurableSet.{u_1} (α := α) {x : α | g x < f x}
Tactic: rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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}
⊢ ∫⁻ (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 ∂μ
have rw₁ : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ g x}
Tactic: rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞
have obtain : ∀ (M : ℝ≥0) (hM : ∀ x ∈ s, f x ≤ (↑M : ℝ≥0∞)), ∫⁻ (x : α) in s, f x ∂μ < ∞
Tactic: obtain ⟨M, hM⟩ := hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ < ∞
have refine : ∫⁻ (x : α) in s, (↑M : ℝ≥0∞) ∂μ < ∞
Tactic: refine lt_of_le_of_lt (setLIntegral_mono measurable_const hM) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ ∫⁻ (x : α) in s, c ∂μ < ∞
have rw : HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
Tactic: rw [lintegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ (↑c : ℝ≥0∞)
⊢ ∫⁻ (x : α), f x ∂μ < ∞
have rw : ∫⁻ (x : α) in univ, f x ∂μ < ∞
Tactic: rw [← μ.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ (↑c : ℝ≥0∞)
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ∞
have refine : ∃ (y : ℝ≥0), ∀ (x : α), Membership.mem (γ := Set α) univ x → f x ≤ (↑y : ℝ≥0∞)
Tactic: refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0
have rw : (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
Tactic: rw [restrict_dirac' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
have pos : a ∈ s → ∫⁻ (x : α), f x ∂dirac a = f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
pos : a ∈ s → ∫⁻ (x : α), f x ∂dirac a = f a
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
have neg : a ∉ s → ∫⁻ (x : α), f x ∂0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0
have rw : (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
Tactic: rw [restrict_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
have pos : a ∈ s → ∫⁻ (x : α), f x ∂dirac a = f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
pos : a ∈ s → ∫⁻ (x : α), f x ∂dirac a = f a
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
have neg : a ∉ s → ∫⁻ (x : α), f x ∂0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a
have rw : Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
Tactic: rw [count, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
have e_f : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a
have rw : Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
Tactic: rw [count, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
have e_f : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ c / ε
have rw : ∀ (tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) (ε_ne_top : ε ≠ ∞),
  ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ c / ε
Tactic: rw [← lintegral_count] at tsum_le_c
Cleared hypotheses: tsum_le_c, ε, ε_ne_zero, ε_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ c / ε
have apply : (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
Tactic: apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ (↑c : ℝ≥0∞) / (↑ε : ℝ≥0∞)
have rw : ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | (↑ε : ℝ≥0∞) ≤ (ofNNReal ∘ a) i} ≤ (↑c : ℝ≥0∞) / (↑ε : ℝ≥0∞)
Tactic: rw [show (fun i => ε ≤ a i) = fun i => (ε : ℝ≥0∞) ≤ ((↑) ∘ a) i by
      simp only [ENNReal.coe_le_coe, Function.comp]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | (↑ε : ℝ≥0∞) ≤ (ofNNReal ∘ a) i} ≤ (↑c : ℝ≥0∞) / (↑ε : ℝ≥0∞)
have this : ∑' (i : α), (ofNNReal ∘ a) i ≤ (↑c : ℝ≥0∞)
Tactic: apply
    ENNReal.count_const_le_le_of_tsum_le (measurable_coe_nnreal_ennreal.comp a_mble) _
      (mod_cast ε_ne_zero) (@ENNReal.coe_ne_top ε)