awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
have mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
Tactic: refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
have mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
have h : ∀ (x : α) (hx : (↑(f x) : ℝ) • g x = g' x) (h'x : (↑(f x) : ℝ≥0∞) ≠ 0), g x = (↑(f x) : ℝ)⁻¹ • g' x
Tactic: filter_upwards [hg'] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ g x = (↑(f x) : ℝ)⁻¹ • g' x
have h : (↑(f x) : ℝ) ≠ 0
Tactic: rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ (↑(f x) : ℝ) ≠ 0
have h'x₁ : ¬f x = 0
Tactic: simp only [Ne, ENNReal.coe_eq_zero] at h'x
Cleared hypotheses: h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (hypothesis)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ FinStronglyMeasurable f μ
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (hypothesis)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ FinStronglyMeasurable f μ
have this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
Tactic: haveI : SeparableSpace (Set.range f ∪ {0} : Set G) :=
    hf_meas.separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (goal)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ FinStronglyMeasurable f μ
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (goal)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable f μ
have refine_2 : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → G) x) atTop (𝓝 (f x))
Tactic: refine ⟨fs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (hypothesis)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h_fs_Lp : ∀ (n : ℕ), MemLp.{u_1, u_2} (ε := G) (⇑(fs n) : (a : α) → G) p μ
Tactic: have h_fs_Lp : ∀ n, MemLp (fs n) p μ :=
      SimpleFunc.memLp_approxOn_range hf_meas.measurable hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (goal)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
x : α
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → G) x) atTop (𝓝 (f x))
have refine_2 : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
Tactic: apply SimpleFunc.tendsto_approxOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp (goal)
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
x : α
⊢ f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
have refine_2 : f x ∈ Set.range f ∪ {0}
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    ∀ ⦃ε : ℝ≥0∞⦄,
      0 < ε →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε
have simp : UnifTight f p μ ↔
  (∀ (r : ℝ≥0),
      0 < r →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑r : ℝ≥0∞)) ∧
    (LT.lt (α := ℝ≥0∞) 0 ∞ →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ∞)
Tactic: simp only [ENNReal.forall_ennreal, ENNReal.coe_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    (∀ (r : ℝ≥0),
        0 < r →
          ∃ (s : Set α),
            Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
              ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑r : ℝ≥0∞)) ∧
      (LT.lt (α := ℝ≥0∞) 0 ∞ →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ∞)
have refine : LT.lt (α := ℝ≥0∞) 0 ∞ →
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ∞
Tactic: refine (and_iff_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ LT.lt (α := ℝ≥0∞) 0 ∞ →
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ∞
have simp : ∃ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [zero_lt_top, le_top, implies_true, and_true, true_implies]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ ∃ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: use ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    ∀ ⦃ε : ℝ⦄,
      0 < ε →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀
  (hut :
    ∀ ⦃ε : ℝ⦄,
      0 < ε →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
  (ε : ℝ≥0) (hε : 0 < ε),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: refine ⟨fun hut rε hrε ↦ hut (Real.toNNReal_pos.mpr hrε), fun hut ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
hut :
  ∀ ⦃ε : ℝ⦄,
    0 < ε →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have obtain : ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal (↑ε : ℝ)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨s, hμs, hfε⟩ := hut hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
hut :
  ∀ ⦃ε : ℝ⦄,
    0 < ε →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal (↑ε : ℝ)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have right : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: use s, hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have pos : ∀ (hε_top : ε = ∞), ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
pos : ∀ (hε_top : ε = ∞), ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have neg : ∀ (hε_top : ¬ε = ∞), ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ε = ∞
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have pos : ∀ (hε : Ne (α := ℝ≥0∞) ∞ 0), ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ∞
Tactic: subst hε_top
Cleared hypotheses: ε, hε, hε_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have neg : ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)),
  ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
Tactic: rcases hf (pos_iff_ne_zero.2 (toNNReal_ne_zero.mpr ⟨hε,hε_top⟩)) with ⟨s, hμs, hfs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have neg : ∀ ⦃s t : Set α⦄,
  s ⊆ t → (∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε) → ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
Tactic: refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)
neg :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε) → ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
have neg₁ : sᶜ ∈ μ.cofinite
Tactic: refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)
⊢ sᶜ ∈ μ.cofinite
have neg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [Measure.compl_mem_cofinite, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have rcases : ∀ (η : ℝ≥0∞) (hη_pos : 0 < η)
  (hη :
    ∀ (f g : α → β),
      AEStronglyMeasurable f μ →
        AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: rcases exists_Lp_half β μ p (coe_ne_zero.mpr hε.ne') with ⟨η, hη_pos, hη⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have pos : ∀ (hη_top : η = ∞),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: by_cases hη_top : η = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
pos :
  ∀ (hη_top : η = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have neg : ∀ (hη_top : ¬η = ∞),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: by_cases hη_top : η = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
hη_top : η = ∞
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have hη₁ : ∀ (f g : α → β),
  AEStronglyMeasurable f μ →
    AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
Tactic: replace hη := hη_top ▸ hη
Cleared hypotheses: hη
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ∞
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have pos : ∀ (i : ι), eLpNorm (indicator ∅ᶜ ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: refine ⟨∅, (by simp), fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ∞
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
i : ι
⊢ eLpNorm (indicator ∅ᶜ ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have pos : eLpNorm (f i + g i) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: simp only [compl_empty, indicator_univ, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
hη_top : ¬η = ∞
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
have neg : ∀ (s : Set α) (hμs : s ∈ μ.cofinite) (hsm : MeasurableSet s) (hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ η)
  (hgs : ∀ (i : ι), eLpNorm (s.indicator (g i)) p μ ≤ η),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨s, hμs, hsm, hfs, hgs⟩ :
      ∃ s ∈ μ.cofinite, MeasurableSet s ∧
        (∀ i, eLpNorm (s.indicator (f i)) p μ ≤ η) ∧
        (∀ i, eLpNorm (s.indicator (g i)) p μ ≤ η) :=
    ((hf.eventually_cofinite_indicator hη_pos.ne').and
      (hg.eventually_cofinite_indicator hη_pos.ne')).exists_measurable_mem_of_smallSets