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)
n : ℕ
a : α
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) (↑(n + 1) : ℝ≥0∞) ≤ 1 a

Tactic:
(ENNReal.div_le_iff_le_mul (Or.inl <| Nat.cast_ne_zero.2 n.succ_ne_zero) <|
      Or.inr one_ne_zero).2 ?_

Premises used: Iff.mpr, ENNReal.div_le_iff_le_mul, Nat.succ_ne_zero, Or.inl, one_ne_zero, Or.inr, Nat.cast_ne_zero
-- 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)
n : ℕ
a : α
refine : ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HMul.hMul (α := ℝ≥0∞) 1 (↑n.succ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) (↑(n + 1) : ℝ≥0∞) ≤ 1 a

Tactic:
refine (ENNReal.div_le_iff_le_mul (Or.inl <| Nat.cast_ne_zero.2 n.succ_ne_zero) <|
      Or.inr one_ne_zero).2 ?_

Premises used: Iff.mpr, ENNReal.div_le_iff_le_mul, Nat.succ_ne_zero, Or.inl, one_ne_zero, Or.inr, Nat.cast_ne_zero
-- 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)
n : ℕ
a : α
rw : ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HSMul.hSMul (β := ℝ≥0∞) (Finset.range n.succ).card 1
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HMul.hMul (α := ℝ≥0∞) 1 (↑n.succ : ℝ≥0∞)

Tactic:
rw [mul_comm, ← nsmul_eq_mul, ← Finset.card_range n.succ]

Premises used: Finset.card_range, mul_comm, nsmul_eq_mul, Nat.succ
-- 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)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HSMul.hSMul (β := ℝ≥0∞) (Finset.range n.succ).card 1

Tactic:
Finset.sum_le_card_nsmul _ _ _ fun _ _ ↦ indicator_le (fun _ _ ↦ le_rfl) _

Premises used: le_rfl, Finset.sum_le_card_nsmul, Set.indicator_le
-- 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)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HSMul.hSMul (β := ℝ≥0∞) (Finset.range n.succ).card 1

Tactic:
exact Finset.sum_le_card_nsmul _ _ _ fun _ _ ↦ indicator_le (fun _ _ ↦ le_rfl) _

Premises used: Finset.sum_le_card_nsmul
-- 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)
⊢ ∀ (n : ℕ), f n ≤ 1

Tactic:
have hf₁ n : f n ≤ 1 := by
    rintro a
    rw [hfapp, ← ENNReal.div_eq_inv_mul]
    refine (ENNReal.div_le_iff_le_mul (Or.inl <| Nat.cast_ne_zero.2 n.succ_ne_zero) <|
      Or.inr one_ne_zero).2 ?_
    rw [mul_comm, ← nsmul_eq_mul, ← Finset.card_range n.succ]
    exact Finset.sum_le_card_nsmul _ _ _ fun _ _ ↦ indicator_le (fun _ _ ↦ le_rfl) _
-- 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
n : ℕ
simp_rw : r ≤ ∫⁻ (a : α), HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) ∂μ
⊢ r ≤ ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [hfapp]
-- 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
n : ℕ
rw : r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ b ∈ Finset.range (n + 1), ∫⁻ (a : α), (s b).indicator 1 a ∂μ)
⊢ r ≤ ∫⁻ (a : α), HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) ∂μ

Tactic:
rw [lintegral_const_mul _ <| Finset.measurable_fun_sum _
        fun _ _ ↦ measurable_one.indicator <| hs _,
      lintegral_finsetSum _ fun _ _ ↦ measurable_one.indicator (hs _)]

Premises used: Measurable.indicator, measurable_one, Finset.measurable_fun_sum, MeasureTheory.lintegral_const_mul, MeasureTheory.lintegral_finsetSum
-- 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
n : ℕ
simp : r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x))
⊢ r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ b ∈ Finset.range (n + 1), ∫⁻ (a : α), (s b).indicator 1 a ∂μ)

Tactic:
simp only [lintegral_indicator_one (hs _)]

Premises used: MeasureTheory.lintegral_indicator_one
-- 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
n : ℕ
⊢ Ne (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞) 0 ∨ Ne (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x)) 0

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
n : ℕ
⊢ Ne (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞) ∞ ∨ Ne (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x)) ∞

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
n : ℕ
rw : (n + 1) • r ≤ ∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x)
⊢ r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x))

Tactic:
rw [← ENNReal.div_eq_inv_mul, ENNReal.le_div_iff_mul_le (by simp) (by simp), ← nsmul_eq_mul']

Premises used: ENNReal.le_div_iff_mul_le, nsmul_eq_mul', ENNReal.div_eq_inv_mul
-- 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
n : ℕ
⊢ (n + 1) • r ≤ ∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x)

Tactic:
simpa using Finset.card_nsmul_le_sum (Finset.range (n + 1)) _ _ fun _ _ ↦ hr _

Premises used: Finset.card_nsmul_le_sum, Finset.range, HAdd.hAdd, 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
⊢ ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ

Tactic:
have hrf n : r ≤ ∫⁻ a, f n a ∂μ := by
    simp_rw [hfapp]
    rw [lintegral_const_mul _ <| Finset.measurable_fun_sum _
        fun _ _ ↦ measurable_one.indicator <| hs _,
      lintegral_finsetSum _ fun _ _ ↦ measurable_one.indicator (hs _)]
    simp only [lintegral_indicator_one (hs _)]
    rw [← ENNReal.div_eq_inv_mul, ENNReal.le_div_iff_mul_le (by simp) (by simp), ← nsmul_eq_mul']
    simpa using Finset.card_nsmul_le_sum (Finset.range (n + 1)) _ _ fun _ _ ↦ hr _
-- 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
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
⊢ False

Tactic:
hr₀ <| le_bot_iff.1 <| hr 0

Premises used: le_bot_iff, Iff.mp, OfNat.ofNat
-- 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
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
⊢ False

Tactic:
exact hr₀ <| le_bot_iff.1 <| hr 0

Premises used: le_bot_iff, Iff.mp, 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 ∂μ
⊢ μ ≠ 0

Tactic:
have hμ : μ ≠ 0 := by rintro rfl; exact hr₀ <| le_bot_iff.1 <| hr 0
-- 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
rw : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ ∫⁻ (x : α), 1 ∂μ
⊢ ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ

Tactic:
rw [← lintegral_one]

Premises used: MeasureTheory.lintegral_one
-- 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
⊢ ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ ∫⁻ (x : α), 1 ∂μ

Tactic:
lintegral_mono fun a ↦ limsup_le_of_le ⟨0, fun R _ ↦ bot_le⟩ <|
      Eventually.of_forall fun n ↦ hf₁ _ _

Premises used: Filter.Eventually.of_forall, Filter.limsup_le_of_le, MeasureTheory.lintegral_mono, Exists.intro, OfNat.ofNat, bot_le