awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
⊢ ∫⁻ (a : α) in s, g n a ∂μ ≤ ∫⁻ (a : α) in s, ⨆ (x : ℕ), g x a ∂μ

Tactic:
lintegral_mono fun x ↦ le_iSup (g · x) n

Premises used: le_iSup, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
a : ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ

Tactic:
calc
    (ψ.map (↑)).lintegral (μ.restrict s) = ∫⁻ a in s, ψ a ∂μ :=
      SimpleFunc.lintegral_eq_lintegral .. |>.symm
    _ ≤ ∫⁻ a in s, min (f a) n ∂μ :=
      lintegral_mono fun a ↦ le_min (hψ _) (ENNReal.coe_le_coe.2 (hn a))
    _ ≤ ∫⁻ a in s, g n a ∂μ := by
      have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)
    _ ≤ _ := lintegral_mono fun x ↦ le_iSup (g · x) n

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.lintegral, MeasureTheory.Measure.restrict, le_iSup, ENNReal.coe_le_coe, le_min, MeasureTheory.lintegral_mono, Eq.symm, MeasureTheory.SimpleFunc.lintegral_eq_lintegral, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
⊢ ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : ∀ n, μ (s n) < ∞ := fun n =>
    (measure_mono <| disjointed_subset _ _).trans_lt (measure_spanningSets_lt_top μ n)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (δ : ℕ → ℝ≥0),
    (∀ (i : ℕ), 0 < δ i) ∧ ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε

Tactic:
ENNReal.exists_pos_tsum_mul_lt_of_countable ε0 _ fun n => (this n).ne

Premises used: ENNReal.exists_pos_tsum_mul_lt_of_countable, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain :
  ∀ (δ : ℕ → ℝ≥0) (δpos : ∀ (i : ℕ), 0 < δ i)
    (δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε),
    ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε

Tactic:
obtain ⟨δ, δpos, δsum⟩ : ∃ δ : ℕ → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, μ (s i) * δ i) < ε :=
    ENNReal.exists_pos_tsum_mul_lt_of_countable ε0 _ fun n => (this n).ne

Premises used: ENNReal.exists_pos_tsum_mul_lt_of_countable, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
⊢ Measurable N

Tactic:
have hN_meas : Measurable N := measurableSet_spanningSetsIndex μ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
⊢ ∀ (n : ℕ), N ⁻¹' {n} = s n

Tactic:
have hNs : ∀ n, N ⁻¹' {n} = s n := preimage_spanningSetsIndex_singleton μ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε

Tactic:
⟨δ ∘ N, fun x => δpos _, measurable_from_nat.comp hN_meas, ?_⟩

Premises used: measurable_from_nat, Measurable.comp, Function.comp, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
refine : ∫⁻ (x : α), (↑((δ ∘ N) x) : ℝ≥0∞) ∂μ < ε
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε

Tactic:
refine ⟨δ ∘ N, fun x => δpos _, measurable_from_nat.comp hN_meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
erw : ∫⁻ (a : ℕ), (↑(δ a) : ℝ≥0∞) ∂map N μ < ε
⊢ ∫⁻ (x : α), (↑((δ ∘ N) x) : ℝ≥0∞) ∂μ < ε

Tactic:
erw [lintegral_comp measurable_from_nat.coe_nnreal_ennreal hN_meas]

Premises used: measurable_from_nat, Measurable.coe_nnreal_ennreal, MeasureTheory.lintegral_comp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (↑(δ i) : ℝ≥0∞) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (a : ℕ), (↑(δ a) : ℝ≥0∞) ∂map N μ < ε

Tactic:
simpa [N, hNs, lintegral_countable', measurableSet_spanningSetsIndex, mul_comm] using δsum

Premises used: MeasureTheory.lintegral_countable', mul_comm, MeasureTheory.measurableSet_spanningSetsIndex
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
⊢ Monotone S

Tactic:
have hS_mono : Monotone S := @monotone_spanningSets _ m (μ.trim hm) _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
⊢ ∀ (n : ℕ), MeasurableSet (S n)

Tactic:
have hS_meas : ∀ n, MeasurableSet[m] (S n) := @measurableSet_spanningSets _ m (μ.trim hm) _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
rw : f (⋃ (i : ℕ), spanningSets (μ.trim hm) i) ≤ C
⊢ f univ ≤ C

Tactic:
rw [← @iUnion_spanningSets _ m (μ.trim hm)]

Premises used: MeasureTheory.Measure.trim, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f (⋃ (i : ℕ), spanningSets (μ.trim hm) i) ≤ C

Tactic:
(h_F_lim S hS_meas hS_mono).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
refine : ⨆ (n : ℕ), f (S n) ≤ C
⊢ f (⋃ (i : ℕ), spanningSets (μ.trim hm) i) ≤ C

Tactic:
refine (h_F_lim S hS_meas hS_mono).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ ⨆ (n : ℕ), f (S n) ≤ C

Tactic:
iSup_le fun n => hf (S n) (hS_meas n) ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
refine : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⨆ (n : ℕ), f (S n) ≤ C

Tactic:
refine iSup_le fun n => hf (S n) (hS_meas n) ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.Measure.trim, MeasureTheory.le_trim, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.Measure.trim, MeasureTheory.le_trim, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
simp only [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
have : ∫⁻ x in univ, f x ∂μ = ∫⁻ x, f x ∂μ := by simp only [Measure.restrict_univ]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
rw : ∫⁻ (x : α) in univ, f x ∂μ ≤ C
⊢ ∫⁻ (x : α), f x ∂μ ≤ C

Tactic:
rw [← this]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α) in univ, f x ∂μ ≤ C

Tactic:
univ_le_of_forall_fin_meas_le hm C hf fun S _ hS_mono => ?_

Premises used: MeasureTheory.univ_le_of_forall_fin_meas_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
refine :
  ∀ (S : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (S n)) →
      ∀ (hS_mono : Monotone S), ∫⁻ (x : α) in ⋃ (n : ℕ), S n, f x ∂μ ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
⊢ ∫⁻ (x : α) in univ, f x ∂μ ≤ C

Tactic:
refine univ_le_of_forall_fin_meas_le hm C hf fun S _ hS_mono => ?_

Premises used: MeasureTheory.univ_le_of_forall_fin_meas_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
h : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
⊢ ∫⁻ (x : α) in ⋃ (n : ℕ), S n, f x ∂μ ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ

Tactic:
rw [setLIntegral_iUnion_of_directed]

Premises used: MeasureTheory.setLIntegral_iUnion_of_directed
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
h : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S

Tactic:
directed_of_isDirected_le hS_mono

Premises used: directed_of_isDirected_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
h : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S

Tactic:
exact directed_of_isDirected_le hS_mono

Premises used: directed_of_isDirected_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
C : ℝ≥0∞
f : α → ℝ≥0∞
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ ≤ C
rwa rwa₁ rwa₂ rwa₃ : SigmaFinite μ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
rwa [trim_eq_self]

Premises used: MeasureTheory.trim_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hs, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
      piecewise_eq_indicator, lintegral_indicator, lintegral_const, Measure.restrict_apply',
      ENNReal.coe_indicator, Function.const_apply] at hL

Premises used: Function.const_apply, MeasureTheory.lintegral_const, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Set.univ_inter, MeasureTheory.lintegral_indicator, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.Measure.restrict_apply', MeasureTheory.SimpleFunc.coe_const, ENNReal.coe_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hc : c = 0
⊢ False

Tactic:
simp only [hc, ENNReal.coe_zero, zero_mul, not_lt_zero] at hL

Premises used: MulZeroClass.zero_mul, ENNReal.not_lt_zero, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ c ≠ 0

Tactic:
have c_ne_zero : c ≠ 0 := by
      intro hc
      simp only [hc, ENNReal.coe_zero, zero_mul, not_lt_zero] at hL
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
h0 : (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0
ht : (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞
⊢ L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rwa [ENNReal.div_lt_iff, mul_comm]

Premises used: mul_comm, ENNReal.div_lt_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0

Tactic:
simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]

Premises used: true_or, Ne, ENNReal.coe_eq_zero, not_false_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞

Tactic:
simp only [Ne, coe_ne_top, not_false_iff, true_or]

Premises used: true_or, Ne, not_false_iff, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
⊢ L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
have : L / c < μ s := by
      rwa [ENNReal.div_lt_iff, mul_comm]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧
        L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Measure.exists_subset_measure_lt_top hs this

Premises used: MeasureTheory.Measure.exists_subset_measure_lt_top