awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ (↑c : ℝ≥0∞)
rw : ∫⁻ (x : α) in univ, f x ∂μ < ∞
⊢ ∫⁻ (x : α), f x ∂μ < ∞

Tactic:
rw [← μ.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 ∂μ < ∞

Tactic:
setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_

Premises used: MeasureTheory.setLIntegral_lt_top_of_le_nnreal, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ (↑c : ℝ≥0∞)
refine : ∃ (y : ℝ≥0), ∀ (x : α), Membership.mem (γ := Set α) univ x → f x ≤ (↑y : ℝ≥0∞)
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ∞

Tactic:
refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_

Premises used: MeasureTheory.setLIntegral_lt_top_of_le_nnreal, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ (↑c : ℝ≥0∞)
⊢ ∃ (y : ℝ≥0), ∀ (x : α), Membership.mem (γ := Set α) univ x → f x ≤ (↑y : ℝ≥0∞)

Tactic:
simpa using f_bdd
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂dirac a = f a

Tactic:
simp [lintegral_congr_ae (ae_eq_dirac' hf)]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_eq_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂dirac a = f a

Tactic:
simp [lintegral_congr_ae (ae_eq_dirac f)]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_eq_dirac
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
rw : (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]

Premises used: MeasureTheory.restrict_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
neg : a ∉ s → ∫⁻ (x : α), f x ∂0 = 0
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
h : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
lintegral_dirac' _ hf

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
h : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
exact lintegral_dirac' _ hf

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
h : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
h : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
exact lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
rw : (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac]

Premises used: MeasureTheory.restrict_dirac
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
neg : a ∉ s → ∫⁻ (x : α), f x ∂0 = 0
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
h : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
lintegral_dirac _ _

Premises used: MeasureTheory.lintegral_dirac
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
h : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
exact lintegral_dirac _ _

Premises used: MeasureTheory.lintegral_dirac
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
h : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
h : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
exact lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
rw : Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
rw [count, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.count, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
e_f : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a

Tactic:
funext fun a => lintegral_dirac' a hf

Premises used: MeasureTheory.lintegral_dirac', funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a

Tactic:
exact funext fun a => lintegral_dirac' a hf

Premises used: MeasureTheory.lintegral_dirac', funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
rw : Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
rw [count, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.count, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
e_f : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) (∑' (a : α), f a)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a

Tactic:
funext fun a => lintegral_dirac a f

Premises used: MeasureTheory.lintegral_dirac, funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (i : α) ↦ ∫⁻ (a : α), f a ∂dirac i) fun (a : α) ↦ f a

Tactic:
exact funext fun a => lintegral_dirac a f

Premises used: MeasureTheory.lintegral_dirac, funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : ε ≠ ∞
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 / ε
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ c / ε

Tactic:
rw [← lintegral_count] at tsum_le_c

Premises used: MeasureTheory.lintegral_count
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : ε ≠ ∞
apply : (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ a i} ≤ c / ε

Tactic:
apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans

Premises used: Measurable.aemeasurable, MeasureTheory.meas_ge_le_lintegral_div, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : ε ≠ ∞
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε

Tactic:
ENNReal.div_le_div tsum_le_c rfl.le

Premises used: Eq.le, ENNReal.div_le_div, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : ε ≠ ∞
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε

Tactic:
exact ENNReal.div_le_div tsum_le_c rfl.le

Premises used: Eq.le, ENNReal.div_le_div, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
⊢ Eq.{u_1 + 1} (α := (i : α) → Prop) (fun (i : α) ↦ ε ≤ a i) fun (i : α) ↦ (↑ε : ℝ≥0∞) ≤ (ofNNReal ∘ a) i

Tactic:
simp only [ENNReal.coe_le_coe, Function.comp]

Premises used: Function.comp, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
rw : ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | (↑ε : ℝ≥0∞) ≤ (ofNNReal ∘ a) i} ≤ (↑c : ℝ≥0∞) / (↑ε : ℝ≥0∞)
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | ε ≤ 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]]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
this : ∑' (i : α), (ofNNReal ∘ a) i ≤ (↑c : ℝ≥0∞)
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) {i : α | (↑ε : ℝ≥0∞) ≤ (ofNNReal ∘ a) i} ≤ (↑c : ℝ≥0∞) / (↑ε : ℝ≥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 ε)

Premises used: Measurable.comp, ENNReal.count_const_le_le_of_tsum_le, measurable_coe_nnreal_ennreal, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
⊢ (↑(∑' (i : α), a i) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)

Tactic:
ENNReal.coe_le_coe.mpr tsum_le_c

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
h : ∑' (i : α), (ofNNReal ∘ a) i = (↑(∑' (i : α), a i) : ℝ≥0∞)
⊢ ∑' (i : α), (ofNNReal ∘ a) i ≤ (↑c : ℝ≥0∞)

Tactic:
convert! ENNReal.coe_le_coe.mpr tsum_le_c

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
h h₁ : (↑(∑' (b : α), a b) : ℝ≥0∞) = (↑(∑' (i : α), a i) : ℝ≥0∞)
⊢ ∑' (i : α), (↑(a i) : ℝ≥0∞) = (↑(∑' (i : α), a i) : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_coe_eq a_summable.hasSum]

Premises used: ENNReal.tsum_coe_eq, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
rw :
  ∑' (i : α), ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i)
| ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← sum_smul_dirac μ, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.sum_smul_dirac, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
conv_lhs :
  Eq (α := ℝ≥0∞)
    (∑' (i : α),
      ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i))
    (∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞))
⊢ ∫⁻ (a : α), f a ∂μ = ∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)

Tactic:
conv_lhs => rw [← sum_smul_dirac μ, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.sum_smul_dirac, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
e_f :
  ∀ (a : α),
    ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) =
      HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : α),
      ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i))
    (∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞))

Tactic:
congr 1 with a : 1
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) =
    HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (x : α) in {a}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)

Tactic:
simp [lintegral_dirac' _ hf, mul_comm]

Premises used: MeasureTheory.lintegral_dirac', mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (x : α) in {a}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
rw rw₁ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ

Tactic:
rw [biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), ∫⁻ (x : α) in {(↑a : α)}, f x ∂μ)
    (∑' (a : (↑s : Type u_1)), HMul.hMul (β := ℝ≥0∞) (f (↑a : α)) ((μ : (a : Set α) → ℝ≥0∞) {(↑a : α)} : ℝ≥0∞))

Tactic:
simp only [lintegral_singleton]

Premises used: MeasureTheory.lintegral_singleton
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
rw : Disjoint s {a}
⊢ ∫⁻ (x : α) in insert a s, f x ∂μ =
    HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) + ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
    add_comm]

Premises used: MeasureTheory.lintegral_singleton, MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.lintegral_union, add_comm, Set.union_singleton
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
rwa rwa₁ rwa₂ rwa₃ : a ∉ s
⊢ Disjoint s {a}

Tactic:
rwa [disjoint_singleton_right]

Premises used: Set.disjoint_singleton_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
s : Finset α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in (↑s : Set α), f x ∂μ = ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) (f x) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)

Tactic:
simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']

Premises used: MeasureTheory.lintegral_countable, Finset.countable_toSet, Finset.tsum_subtype'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
inst_2 : Fintype α
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in (↑Finset.univ : Set α), f x ∂μ
rw₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in univ, f x ∂μ
rw₂ rw₃ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x : α, HMul.hMul (β := ℝ≥0∞) (f x) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)

Tactic:
rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]

Premises used: Finset.coe_univ, MeasureTheory.lintegral_finset, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Unique α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = HMul.hMul (β := ℝ≥0∞) (f default) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
calc
    ∫⁻ x, f x ∂μ = ∫⁻ _, f default ∂μ := lintegral_congr <| Unique.forall_iff.2 rfl
    _ = f default * μ univ := lintegral_const _

Premises used: Iff.mpr, MeasureTheory.lintegral_const, Trans.trans, Unique.forall_iff, MeasureTheory.lintegral_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
rsuffices :
  ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgle : g ≤ f)
    (hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
rsuffices₁ : ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
rsuffices ⟨g, hgm, hgle, hleg⟩ :
      ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgle : g ≤ f
hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩

Premises used: LE.le.antisymm, MeasureTheory.lintegral_mono, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgle : g ≤ f
hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
exact ⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
inr :
  ∀
    (this :
      ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
        ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ)
    (h : ¬IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
wlog :
  ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
wlog h : IsFiniteMeasure μ generalizing μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
inr :
  ∀ (g : (n : ℕ) → α → ℝ≥0∞) (hgm : ∀ (n : ℕ), Measurable (g n)) (hgle : ∀ (n : ℕ), g n ≤ f)
    (hgint : ∀ (n : ℕ) (s : Set α), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ n ≤ ∫⁻ (a : α) in s, g n a ∂sfiniteSeq μ n),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance

Premises used: inferInstance, MeasureTheory.sfiniteSeq