awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
u : Set ℕ
hux : u ⊆ {n : ℕ | x ∈ s n}
hu : u.Finite
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ hu.toFinset (s := u), s n) : ℝ≥0∞)

Tactic:
exact hN₁ _ ⟨x, mem_iInter₂.2 fun n hn ↦ hux <| hu.mem_toFinset.1 hn, hxN⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Set.mem_iInter₂, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
⊢ ∀ᶠ (a : ℕ) in atTop, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f a x ∂μ) 1

Tactic:
Eventually.of_forall fun n ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
refine_1 : ∀ (n : ℕ), (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f n x ∂μ) 1
⊢ ∀ᶠ (a : ℕ) in atTop, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f a x ∂μ) 1

Tactic:
refine Eventually.of_forall fun n ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
refine_1 :
  ∀ [IsFiniteMeasure.{u_2} (α := α) (m0 := inst) 0] (hr : ∀ (n : ℕ), r ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) (s n)),
    let M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup (m0 := inst) f 0 < (↑‖f x‖₊ : ℝ≥0∞)};
    let N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1);
    ∀ (hN₀ : Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞))
      (hN₁ :
        ∀ (u : Finset ℕ),
          ((⋂ n ∈ u, s n) \ N).Nonempty →
            LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞))
      (hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂0) (hμ : Ne.{u_2 + 1} (α := Measure α) 0 0)
      (this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂0 ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)
      (hxN : x ∉ N) (hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂0 ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop),
      ⨍⁻ (x : α), f n x ∂0 ≤ 1
refine_1₁ : NeZero μ → ⨍⁻ (x : α), f n x ∂μ ≤ 1
⊢ (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f n x ∂μ) 1

Tactic:
obtain rfl | _ := eq_zero_or_neZero μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
x : α
n : ℕ
inst_1 : IsFiniteMeasure.{u_2} (α := α) (m0 := inst) 0
hr : ∀ (n : ℕ), r ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup (m0 := inst) f 0 < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty →
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂0
hμ : Ne.{u_2 + 1} (α := Measure α) 0 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂0 ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂0 ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
⊢ ⨍⁻ (x : α), f n x ∂0 ≤ 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
h : NeZero μ
refine_1 : ⨍⁻ (x : α), f n x ∂μ ≤ ⨍⁻ (_x : α), 1 ∂μ
⊢ ⨍⁻ (x : α), f n x ∂μ ≤ 1

Tactic:
rw [← laverage_const μ 1]

Premises used: MeasureTheory.laverage_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
h : NeZero μ
⊢ ⨍⁻ (x : α), f n x ∂μ ≤ ⨍⁻ (_x : α), 1 ∂μ

Tactic:
lintegral_mono (hf₁ _)

Premises used: MeasureTheory.laverage, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
h : NeZero μ
⊢ ⨍⁻ (x : α), f n x ∂μ ≤ ⨍⁻ (_x : α), 1 ∂μ

Tactic:
exact lintegral_mono (hf₁ _)

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
refine_2 : ∀ (n : ℕ) (hn : ⨍⁻ (x : α), f n x ∂μ ≤ b), HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b

Tactic:
obtain ⟨n, hn⟩ := hb.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
n : ℕ
hn : ⨍⁻ (x : α), f n x ∂μ ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f n x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b

Tactic:
rw [laverage_eq] at hn

Premises used: MeasureTheory.laverage_eq
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
n : ℕ
hn : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f n x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b

Tactic:
(ENNReal.div_le_div_right (hrf _) _).trans hn

Premises used: ENNReal.div_le_div_right, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
n : ℕ
hn : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f n x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b

Tactic:
exact (ENNReal.div_le_div_right (hrf _) _).trans hn

Premises used: ENNReal.div_le_div_right, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
obtain :
  ∀ (t : Set ℕ) (ht : t.Infinite)
    (h :
      ∀ ⦃u : Set ℕ⦄,
        u ⊆ t →
          u.Finite →
            LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)),
    ∃ (t : Set ι),
      t.Infinite ∧
        ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)
⊢ ∃ (t : Set ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)

Tactic:
obtain ⟨t, ht, h⟩ := bergelson' (fun n ↦ hs <| Infinite.natEmbedding _ n) hr₀ (fun n ↦ hr _)

Premises used: bergelson', DFunLike.coe, Infinite.natEmbedding
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
t : Set ℕ
ht : t.Infinite
h :
  ∀ ⦃u : Set ℕ⦄,
    u ⊆ t →
      u.Finite →
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)
⊢ ∃ (t : Set ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)

Tactic:
⟨_, ht.image <| (Infinite.natEmbedding _).injective.injOn, fun u hut hu ↦
    (h (preimage_subset_of_surjOn (Infinite.natEmbedding _).injective hut) <| hu.preimage
    (Embedding.injective _).injOn).trans_le <| measure_mono <| subset_iInter₂ fun i hi ↦ ?_⟩

Premises used: Set.Infinite.image, Function.Injective.injOn, Set.subset_iInter₂, LT.lt.trans_le, And.intro, MeasureTheory.measure_mono, Exists.intro, Function.Embedding.injective, Set.preimage_subset_of_surjOn, Infinite.natEmbedding, Set.Finite.preimage
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
t : Set ℕ
ht : t.Infinite
h :
  ∀ ⦃u : Set ℕ⦄,
    u ⊆ t →
      u.Finite →
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)
refine :
  ∀ (u : Set ι) (hut : u ⊆ (⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) '' t) (hu : u.Finite) (i : ι) (hi : i ∈ u),
    ⋂ (n : ℕ),
        ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
          s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
      s i
⊢ ∃ (t : Set ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)

Tactic:
refine ⟨_, ht.image <| (Infinite.natEmbedding _).injective.injOn, fun u hut hu ↦
    (h (preimage_subset_of_surjOn (Infinite.natEmbedding _).injective hut) <| hu.preimage
    (Embedding.injective _).injOn).trans_le <| measure_mono <| subset_iInter₂ fun i hi ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
t : Set ℕ
ht : t.Infinite
h :
  ∀ ⦃u : Set ℕ⦄,
    u ⊆ t →
      u.Finite →
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)
u : Set ι
hut : u ⊆ (⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) '' t
hu : u.Finite
i : ι
hi : i ∈ u
obtain :
  ∀ (n : ℕ) (hi : Membership.mem (α := ι) u ((Infinite.natEmbedding ι : (a : ℕ) → ι) n : ι)),
    ⋂ (n : ℕ),
        ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
          s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
      s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)
⊢ ⋂ (n : ℕ),
      ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
        s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
    s i

Tactic:
obtain ⟨n, -, rfl⟩ := hut hi

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
t : Set ℕ
ht : t.Infinite
h :
  ∀ ⦃u : Set ℕ⦄,
    u ⊆ t →
      u.Finite →
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)
u : Set ι
hut : u ⊆ (⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) '' t
hu : u.Finite
n : ℕ
hi : Membership.mem (α := ι) u ((Infinite.natEmbedding ι : (a : ℕ) → ι) n : ι)
⊢ ⋂ (n : ℕ),
      ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
        s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
    s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)

Tactic:
iInter₂_subset n hi

Premises used: Set.iInter₂_subset