awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : Eq.{u_3 + 1} (α := 𝕜) ((↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x)),
  HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x
Tactic: filter_upwards [Lp.coeFn_zero 𝕜 p μ] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
x : α
hx : Eq.{u_3 + 1} (α := 𝕜) ((↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x)
⊢ HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (0 x) ((↑(↑f : α →ₘ[μ] E) : α → E) x) = 0 x
Tactic: rw [Pi.smul_apply', hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ c • f • g = f • c • g
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [smul_def, ← MemLp.toLp_const_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hfg : c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)
Tactic: apply MemLp.toLp_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)
have h : ∀ (x : α) (hfx : (↑(↑(c • f) : α →ₘ[μ] 𝕜) : α → 𝕜) x = (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜)) x)
  (hgx : (↑(↑(c • g) : α →ₘ[μ] E) : α → E) x = (c • (↑(↑g : α →ₘ[μ] E) : α → E)) x),
  (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
    ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)) x
Tactic: filter_upwards [Lp.coeFn_smul c f, Lp.coeFn_smul c g] with x hfx hgx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
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)
⊢ ∃ (t : Set ℕ),
    t.Infinite ∧
      ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hN₀ : μ N = 0 := measure_iUnion_null fun u ↦ meas_eLpNormEssSup_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
⊢ ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have simp_rw : ((⋂ n ∈ u, s n) \ N).Nonempty → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have refine : x ∈ M (indicator (⋂ n ∈ u, s n) 1)
Tactic: refine hx.2 (mem_iUnion.2 ⟨u, ?_⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ M (indicator (⋂ n ∈ u, s n) 1)
have rw : 0 < (↑(nnnorm (E := ℝ) (1 x)) : ℝ≥0∞)
Tactic: rw [mem_setOf, indicator_of_mem hx.1, eLpNormEssSup_eq_zero_iff.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : 0 < (↑(nnnorm (E := ℝ) (1 x)) : ℝ≥0∞)
⊢ x ∈ M (indicator (⋂ n ∈ u, s n) 1)
have rw₁ : (ae μ).EventuallyEq (β := ℝ) (indicator (⋂ n ∈ u, s n) 1) 0
Tactic: rw [mem_setOf, indicator_of_mem hx.1, eLpNormEssSup_eq_zero_iff.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ) (indicator (⋂ n ∈ u, s n) 1) 0
have rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋂ n ∈ u, s n) ∩ support (M := ℝ) 1) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [indicator_ae_eq_zero, Function.support_one, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋂ n ∈ u, s n) ∩ support (M := ℝ) 1) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ) (indicator (⋂ n ∈ u, s n) 1) 0
have rwa₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋂ n ∈ u, s n) ∩ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [indicator_ae_eq_zero, Function.support_one, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
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∞)
⊢ ∃ (t : Set ℕ),
    t.Infinite ∧
      ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have hN₁ : ∀ (u : Finset ℕ),
  ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
Tactic: have hN₁ (u : Finset ℕ) : ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n) := by
    simp_rw [pos_iff_ne_zero]
    rintro ⟨x, hx⟩ hu
    refine hx.2 (mem_iUnion.2 ⟨u, ?_⟩)
    rw [mem_setOf, indicator_of_mem hx.1, eLpNormEssSup_eq_zero_iff.2]
    · simp
    · rwa [indicator_ae_eq_zero, Function.support_one, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
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)
⊢ ∃ (t : Set ℕ),
    t.Infinite ∧
      ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have hfapp : ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
Tactic: have hfapp : ∀ n a, f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a := by
    simp only [f, Pi.smul_apply, Finset.sum_apply,
    forall_const, imp_true_iff, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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)
n : ℕ
⊢ Measurable (f n)
have funProp : ∀ i ∈ Finset.range (n + 1), MeasurableSet (s i)
Tactic: fun_prop (disch := exact hs _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
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)
⊢ ∃ (t : Set ℕ),
    t.Infinite ∧
      ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have hf : ∀ (n : ℕ), Measurable (f n)
Tactic: have hf n : Measurable (f n) := by fun_prop (disch := exact hs _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 : α
⊢ f n a ≤ 1 a
have rw : HDiv.hDiv (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) (↑(n + 1) : ℝ≥0∞) ≤ 1 a
Tactic: rw [hfapp, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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
have refine : ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HMul.hMul (α := ℝ≥0∞) 1 (↑n.succ : ℝ≥0∞)
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 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 ≤ HMul.hMul (α := ℝ≥0∞) 1 (↑n.succ : ℝ≥0∞)
have rw : ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ HSMul.hSMul (β := ℝ≥0∞) (Finset.range n.succ).card 1
Tactic: rw [mul_comm, ← nsmul_eq_mul, ← Finset.card_range n.succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
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)
⊢ ∃ (t : Set ℕ),
    t.Infinite ∧
      ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
have hf₁ : ∀ (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) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 ∂μ
have simp_rw : r ≤ ∫⁻ (a : α), HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) ∂μ
Tactic: simp_rw [hfapp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 : α), HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) ∂μ
have rw : r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ b ∈ Finset.range (n + 1), ∫⁻ (a : α), (s b).indicator 1 a ∂μ)
Tactic: rw [lintegral_const_mul _ <| Finset.measurable_fun_sum _
        fun _ _ ↦ measurable_one.indicator <| hs _,
      lintegral_finsetSum _ fun _ _ ↦ measurable_one.indicator (hs _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ b ∈ Finset.range (n + 1), ∫⁻ (a : α), (s b).indicator 1 a ∂μ)
have simp : r ≤ HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ x ∈ Finset.range (n + 1), (μ : (a : Set α) → ℝ≥0∞) (s x))
Tactic: simp only [lintegral_indicator_one (hs _)]