awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
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 : α
refine_2 : f x ∈ Set.range f ∪ {0}
⊢ f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
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 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ AEFinStronglyMeasurable f μ

Tactic:
⟨hf.aestronglyMeasurable.mk f,
    ((memLp_congr_ae hf.aestronglyMeasurable.ae_eq_mk).mp
          hf).finStronglyMeasurable_of_stronglyMeasurable
      hf.aestronglyMeasurable.stronglyMeasurable_mk hp_ne_zero hp_ne_top,
    hf.aestronglyMeasurable.ae_eq_mk⟩

Premises used: MeasureTheory.memLp_congr_ae, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, Iff.mp, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : Integrable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
(memLp_one_iff_integrable.mpr hf).aefinStronglyMeasurable one_ne_zero ENNReal.coe_ne_top

Premises used: Iff.mpr, MeasureTheory.MemLp.aefinStronglyMeasurable, one_ne_zero, MeasureTheory.memLp_one_iff_integrable, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : ↥(Lp G p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ FinStronglyMeasurable (↑(↑f : α →ₘ[μ] G) : α → G) μ

Tactic:
(Lp.memLp f).finStronglyMeasurable_of_stronglyMeasurable (Lp.stronglyMeasurable f) hp_ne_zero
    hp_ne_top

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
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 μ ≤ ∞)
⊢ UnifTight f p μ ↔
    ∀ ⦃ε : ℝ≥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]

Premises used: ENNReal.coe_pos, ENNReal.forall_ennreal
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ ≤ ∞)

Tactic:
(and_iff_left ?_).symm

Premises used: and_iff_left, MeasureTheory.UnifTight, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
refine :
  LT.lt (α := ℝ≥0∞) 0 ∞ →
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ∞
⊢ 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:
refine (and_iff_left ?_).symm

Premises used: and_iff_left, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
simp : ∃ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥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 [zero_lt_top, le_top, implies_true, and_true, true_implies]

Premises used: ENNReal.zero_lt_top, and_true, le_top, true_implies, implies_true
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
use ∅
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [measure_empty] using zero_ne_top

Premises used: ENNReal.zero_ne_top, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 ε

Tactic:
⟨fun hut rε hrε ↦ hut (Real.toNNReal_pos.mpr hrε), fun hut ε hε ↦ ?_⟩

Premises used: Iff.mpr, Real.toNNReal_pos, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
x : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
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∞)
⊢ UnifTight f p μ ↔
    ∀ ⦃ε : ℝ⦄,
      0 < ε →
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨fun hut rε hrε ↦ hut (Real.toNNReal_pos.mpr hrε), fun hut ε hε ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 < ε
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∞)
⊢ ∃ (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ε
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (↑ε : ℝ)
right : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
use s, hμs
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (↑ε : ℝ)
i : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
(hfε i).trans_eq (ofReal_coe_nnreal (p := ε))

Premises used: LE.le.trans_eq, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (↑ε : ℝ)
i : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact (hfε i).trans_eq (ofReal_coe_nnreal (p := ε))

Premises used: LE.le.trans_eq, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ ≤ ε
neg : ∀ (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 μ ≤ ε

Tactic:
by_cases hε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : ε = ∞
pos :
  ∀ (hε : Ne (α := ℝ≥0∞) ∞ 0), ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ∞
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
subst hε_top
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hε : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : ¬ε = ∞
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 μ ≤ ε
⊢ ∀ᶠ (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⟩

Premises used: Iff.mpr, ENNReal.toNNReal_ne_zero, And.intro, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ ≤ ε

Tactic:
(eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩

Premises used: ENNReal.coe_toNNReal, Iff.mpr, Compl.compl, Eq.rec, And.intro, Exists.intro, Filter.eventually_smallSets'
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ ≤ ε
neg₁ : sᶜ ∈ μ.cofinite
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩

Premises used: Iff.mpr, Compl.compl, And.intro, Exists.intro, Filter.eventually_smallSets'
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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_1 : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ (i : ι), eLpNorm (s_1ᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)
s t : Set α
hst : s ⊆ t
ht : ∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε
i : ι
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
(eLpNorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)

Premises used: MeasureTheory.eLpNorm_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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_1 : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ (i : ι), eLpNorm (s_1ᶜ.indicator (f i)) p μ ≤ (↑ε.toNNReal : ℝ≥0∞)
s t : Set α
hst : s ⊆ t
ht : ∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε
i : ι
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
exact (eLpNorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)

Premises used: MeasureTheory.eLpNorm_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
neg₁ neg₂ neg₃ neg₄ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ sᶜ ∈ μ.cofinite

Tactic:
rwa [Measure.compl_mem_cofinite, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, MeasureTheory.Measure.compl_mem_cofinite
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 α
hμs : s ∈ μ.cofinite
hsm : MeasurableSet s
hfs rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
⊢ ∀ (i : ι), eLpNorm (sᶜᶜ.indicator (f i)) p μ ≤ ε

Tactic:
rwa [compl_compl s]

Premises used: compl_compl
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 < ε
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∞)
⊢ ∃ (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η⟩

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', MeasureTheory.exists_Lp_half
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
neg :
  ∀ (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∞)

Tactic:
by_cases hη_top : η = ∞
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : η = ∞
⊢ ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)

Tactic:
replace hη := hη_top ▸ hη
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
pos : ∀ (i : ι), eLpNorm (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∞)

Tactic:
refine ⟨∅, (by simp), fun i ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : ι
pos : eLpNorm (f i + g i) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm (indicator ∅ᶜ ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
simp only [compl_empty, indicator_univ, Pi.add_apply]

Premises used: Pi.add_apply, Set.indicator_univ, Set.compl_empty
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (f i + g i) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
(hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le

Premises used: LT.lt.le, le_top
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (f i + g i) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact (hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le

Premises used: LT.lt.le, le_top