awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ¬η = ∞
⊢ ∃ s ∈ μ.cofinite,
    MeasurableSet s ∧ (∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ η) ∧ ∀ (i : ι), eLpNorm (s.indicator (g i)) p μ ≤ η

Tactic:
((hf.eventually_cofinite_indicator hη_pos.ne').and
      (hg.eventually_cofinite_indicator hη_pos.ne')).exists_measurable_mem_of_smallSets

Premises used: Filter.Eventually.exists_measurable_mem_of_smallSets, Filter.Eventually.and, MeasureTheory.UnifTight.eventually_cofinite_indicator, LT.lt.ne'
-- 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 : ¬η = ∞
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∞)
⊢ ∃ (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

Premises used: Filter.Eventually.exists_measurable_mem_of_smallSets, Filter.Eventually.and, MeasureTheory.UnifTight.eventually_cofinite_indicator, MeasureTheory.Measure.cofinite, LT.lt.ne'
-- 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 : ¬η = ∞
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:
⟨sᶜ, ne_of_lt hμs, fun i ↦ ?_⟩

Premises used: Compl.compl, And.intro, Exists.intro, ne_of_lt
-- 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 : ¬η = ∞
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 μ ≤ η
neg : ∀ (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:
refine ⟨sᶜ, ne_of_lt hμs, 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η :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
hη_top : ¬η = ∞
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 μ ≤ η
i : ι
⊢ (↑η.toNNReal : ℝ≥0∞) = η

Tactic:
have η_cast : ↑η.toNNReal = η := coe_toNNReal 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 : ¬η = ∞
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 μ ≤ η
i : ι
η_cast : (↑η.toNNReal : ℝ≥0∞) = η
rw : eLpNorm (s.indicator (f i + g i)) p μ = eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ
rw₁ rw₂ : eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ = eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ
⊢ eLpNorm (sᶜᶜ.indicator (f i + g i)) p μ = eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ

Tactic:
rw [compl_compl, indicator_add']

Premises used: compl_compl, Set.indicator_add'
-- 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 : ¬η = ∞
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 μ ≤ η
i : ι
η_cast : (↑η.toNNReal : ℝ≥0∞) = η
⊢ eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
le_of_lt <|
      hη _ _ ((hf_meas i).indicator hsm) ((hg_meas i).indicator hsm)
        (η_cast ▸ hfs i) (η_cast ▸ hgs i)

Premises used: le_of_lt, Eq.rec, MeasureTheory.AEStronglyMeasurable.indicator, Eq.symm
-- 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 μ →
        MeasureTheory.eLpNorm f p μ ≤ η →
          MeasureTheory.eLpNorm g p μ ≤ η → MeasureTheory.eLpNorm (f + g) p μ < (↑ε : ℝ≥0∞)
hη_top : ¬η = ∞
s : Set α
hμs : s ∈ μ.cofinite
hsm : MeasurableSet s
hfs : ∀ (i : ι), MeasureTheory.eLpNorm (s.indicator (f i)) p μ ≤ η
hgs : ∀ (i : ι), MeasureTheory.eLpNorm (s.indicator (g i)) p μ ≤ η
i : ι
η_cast : (↑η.toNNReal : ℝ≥0∞) = η
eLpNorm :
  MeasureTheory.eLpNorm (sᶜᶜ.indicator (f i + g i)) p μ =
    MeasureTheory.eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ
⊢ MeasureTheory.eLpNorm (sᶜᶜ.indicator ((f + g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
calc
    eLpNorm (indicator sᶜᶜ (f i + g i)) p μ
      = eLpNorm (indicator s (f i) + indicator s (g i)) p μ := by rw [compl_compl, indicator_add']
    _ ≤ ε := le_of_lt <|
      hη _ _ ((hf_meas i).indicator hsm) ((hg_meas i).indicator hsm)
        (η_cast ▸ hfs i) (η_cast ▸ hgs i)

Premises used: Set.indicator, Compl.compl, le_of_lt, Eq.rec, HAdd.hAdd, MeasureTheory.AEStronglyMeasurable.indicator, Eq.symm, MeasureTheory.eLpNorm
-- 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 μ
simp_rw :
  ∀ ⦃ε : ℝ≥0⦄,
    0 < ε →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ UnifTight (-f) p μ

Tactic:
simp_rw [UnifTight, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]

Premises used: Set.indicator_neg', MeasureTheory.eLpNorm_neg, MeasureTheory.UnifTight, Pi.neg_apply
-- 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⦄,
    0 < ε →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
hf

Premises used: MeasureTheory.UnifTight
-- 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⦄,
    0 < ε →
      ∃ (s : Set α),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact hf
-- 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) μ
rw : UnifTight (f + -g) p μ
⊢ UnifTight (f - g) p μ

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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) μ
⊢ UnifTight (f + -g) p μ

Tactic:
hf.add hg.neg hf_meas fun i => (hg_meas i).neg

Premises used: MeasureTheory.UnifTight.add, MeasureTheory.AEStronglyMeasurable.neg, MeasureTheory.UnifTight.neg
-- 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) μ
⊢ UnifTight (f + -g) p μ

Tactic:
exact hf.add hg.neg hf_meas fun i => (hg_meas i).neg

Premises used: MeasureTheory.UnifTight.add, MeasureTheory.AEStronglyMeasurable.neg, MeasureTheory.UnifTight.neg
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ≥0
hε : 0 < ε
obtain :
  ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨s, hμs, hfε⟩ := hf 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
⟨s, hμs, fun n => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfε n)⟩

Premises used: And.intro, Exists.intro, LE.le.trans, le_of_eq, MeasureTheory.eLpNorm_congr_ae
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
refine : ∀ (n : ι), sᶜ.indicator (g n) =ᶠ[ae μ] sᶜ.indicator (f n)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
refine ⟨s, hμs, fun n => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfε n)⟩
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ι
h : ∀ (x : α) (hx : f n x = g n x), sᶜ.indicator (g n) x = sᶜ.indicator (f n) x
⊢ sᶜ.indicator (g n) =ᶠ[ae μ] sᶜ.indicator (f n)

Tactic:
filter_upwards [hfg n] with x hx
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ι
x : α
hx : f n x = g n x
⊢ sᶜ.indicator (g n) x = sᶜ.indicator (f n) x

Tactic:
simp only [indicator, mem_compl_iff, hx]

Premises used: Set.indicator, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
⊢ UnifTight f p μ ↔ UnifTight g p μ

Tactic:
⟨fun h => h.aeeq hfg, fun h => h.aeeq fun i => (hfg i).symm⟩

Premises used: Iff.intro, MeasureTheory.UnifTight.aeeq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
pos :
  ∀ (hε_top : (↑ε : ℝ≥0∞) = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)
neg :
  ∀ (hε_top : ¬(↑ε : ℝ≥0∞) = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ 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 β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : (↑ε : ℝ≥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 β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : (↑ε : ℝ≥0∞) = ∞
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
neg :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
        (hgε : eLpNorm (sᶜ.indicator g) p μ < (↑ε : ℝ≥0∞)),
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨s, _, hμs, hgε⟩ := hg.exists_eLpNorm_indicator_compl_lt hp_ne_top (coe_ne_zero.mpr hε.ne')

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (sᶜ.indicator g) p μ < (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
⟨s, ne_of_lt hμs, fun _ => hgε.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (sᶜ.indicator g) p μ < (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm.{u_1, u_2} (ε := β) (sᶜ.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact ⟨s, ne_of_lt hμs, fun _ => hgε.le⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
pos :
  ∀ (hε_top : (↑ε : ℝ≥0∞) = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
neg :
  ∀ (hε_top : ¬(↑ε : ℝ≥0∞) = ∞),
    ∃ (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:
by_cases hε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : (↑ε : ℝ≥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 β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : (↑ε : ℝ≥0∞) = ∞
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact ⟨∅, by simp, fun _ => hε_top.symm ▸ le_top⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
pos :
  ∀ (hι : Nonempty ι),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
by_cases :
  ∀ (hι : ¬Nonempty ι),
    ∃ (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:
by_cases hι : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
hι : ¬Nonempty ι
⊢ 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 β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
hι : ¬Nonempty ι
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact ⟨∅, (by simp), fun i => False.elim <| hι <| Nonempty.intro i⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
hι : ¬Nonempty ι
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
case neg => exact ⟨∅, (by simp), fun i => False.elim <| hι <| Nonempty.intro i⟩