awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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)
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
have a : ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞)
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε
have 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∞) ∂μ < ε
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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 μ
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε
have hN_meas : Measurable N
Tactic: have hN_meas : Measurable N := measurableSet_spanningSetsIndex μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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
⊢ ∃ (g : α → ℝ≥0), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ε
have hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
Tactic: have hNs : ∀ n, N ⁻¹' {n} = s n := preimage_spanningSetsIndex_singleton μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ < ε
have refine : ∫⁻ (x : α), (↑((δ ∘ N) x) : ℝ≥0∞) ∂μ < ε
Tactic: refine ⟨δ ∘ N, fun x => δpos _, measurable_from_nat.comp hN_meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
⊢ ∫⁻ (x : α), (↑((δ ∘ N) x) : ℝ≥0∞) ∂μ < ε
have erw : ∫⁻ (a : ℕ), (↑(δ a) : ℝ≥0∞) ∂map N μ < ε
Tactic: erw [lintegral_comp measurable_from_nat.coe_nnreal_ennreal hN_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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)
⊢ f univ ≤ C
have hS_mono : Monotone S
Tactic: have hS_mono : Monotone S := @monotone_spanningSets _ m (μ.trim hm) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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
⊢ f univ ≤ C
have hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
Tactic: have hS_meas : ∀ n, MeasurableSet[m] (S n) := @measurableSet_spanningSets _ m (μ.trim hm) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 univ ≤ C
have rw : f (⋃ (i : ℕ), spanningSets (μ.trim hm) i) ≤ C
Tactic: rw [← @iUnion_spanningSets _ m (μ.trim hm)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
have refine : ⨆ (n : ℕ), f (S n) ≤ C
Tactic: refine (h_F_lim S hS_meas hS_mono).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
have refine : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine iSup_le fun n => hf (S n) (hS_meas n) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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 : α), f x ∂μ ≤ C
have this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: have : ∫⁻ x in univ, f x ∂μ = ∫⁻ x, f x ∂μ := by simp only [Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 : α), f x ∂μ ≤ C
have rw : ∫⁻ (x : α) in univ, f x ∂μ ≤ C
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
have 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 ∂μ
Tactic: refine univ_le_of_forall_fin_meas_le hm C hf fun S _ hS_mono => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
⊢ ∫⁻ (x : α) in ⋃ (n : ℕ), S n, f x ∂μ ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
have hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
Tactic: rw [setLIntegral_iUnion_of_directed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have hL₁ : 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
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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∞)
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have c_ne_zero : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
have h0 : (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0
Tactic: rwa [ENNReal.div_lt_iff, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
⊢ L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
have ht : (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞
Tactic: rwa [ENNReal.div_lt_iff, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have const : ∀ (t : Set α) (ht : MeasurableSet t) (ts : t ⊆ s) (mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t)
  (t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: obtain ⟨t, ht, ts, mlt, t_top⟩ :
      ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
      Measure.exists_subset_measure_lt_top hs this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have const : ∀ (x : α),
  LE.le (α := ℝ≥0) ((piecewise t ht (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const :
  ∀ (x : α),
    LE.le (α := ℝ≥0) ((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
      ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have const₁ : ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
Tactic: refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const :
  ∀ (x : α),
    LE.le (α := ℝ≥0) ((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
      ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
const₁ : ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have const₂ : L < ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
⊢ LE.le (α := ℝ≥0) ((piecewise t ht (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
have const : ∀ (x : α), LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (0 x : ℝ≥0) (((const α c : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine indicator_le_indicator_of_subset ts (fun x => ?_) x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ L < ∫⁻ (x : α), (↑((piecewise t ht (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have const : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have const : (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0
Tactic: rwa [mul_comm, ← ENNReal.div_lt_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const : (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0
⊢ L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have const₁ : (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞
Tactic: rwa [mul_comm, ← ENNReal.div_lt_iff]