awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)
i : Fin (n + 1)
pos : ∀ (hi : (↑i : ℕ) < n), eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have neg : ∀ (hi : n ≤ (↑i : ℕ)), eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: by_cases! hi : i.val < n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)
i : Fin (n + 1)
hi : (↑i : ℕ) < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have pos : eLpNorm (sᶜ.indicator (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n)))) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: rw [show f i = g ⟨i.val, hi⟩ from rfl, compl_union, ← indicator_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)
i : Fin (n + 1)
hi : (↑i : ℕ) < n
⊢ eLpNorm (sᶜ.indicator (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n)))) p μ ≤ (↑ε : ℝ≥0∞)
have pos : eLpNorm (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n))) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: apply (eLpNorm_indicator_le _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)
i : Fin (n + 1)
hi : n ≤ (↑i : ℕ)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have neg : ∀ (hi : n ≤ (↑(Fin.last n) : ℕ)), eLpNorm ((s ∪ S)ᶜ.indicator (f (Fin.last n))) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain rfl : i = Fin.last n := Fin.ext (le_antisymm i.is_le hi)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)
hi : n ≤ (↑(Fin.last n) : ℕ)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f (Fin.last n))) p μ ≤ (↑ε : ℝ≥0∞)
have neg : eLpNorm (Sᶜ.indicator (sᶜ.indicator (f (Fin.last n)))) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: rw [compl_union, inter_comm, ← indicator_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
⊢ ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
have zero : ∀ {f : Fin 0 → α → β} (hf : ∀ (i : Fin 0), MemLp (f i) p μ), UnifTight f p μ
Tactic: induction n with
  | zero => exact fun {f} hf ↦ unifTight_of_subsingleton hp_top hf
  | succ n h =>
    intro f hfLp ε hε
    by_cases hε_top : ε = ∞
    · exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
    let g : Fin n → α → β := fun k => f k.castSucc
    have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
    obtain ⟨S, hμS, hFε⟩ := h hgLp hε
    obtain ⟨s, _, hμs, hfε⟩ :=
      (hfLp (Fin.last n)).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')
    refine ⟨s ∪ S, (by finiteness), fun i => ?_⟩
    by_cases! hi : i.val < n
    · rw [show f i = g ⟨i.val, hi⟩ from rfl, compl_union, ← indicator_indicator]
      apply (eLpNorm_indicator_le _).trans
      exact hFε (Fin.castLT i hi)
    · obtain rfl : i = Fin.last n := Fin.ext (le_antisymm i.is_le hi)
      rw [compl_union, inter_comm, ← indicator_indicator]
      exact (eLpNorm_indicator_le _).trans hfε.le
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
zero : ∀ {f : Fin 0 → α → β} (hf : ∀ (i : Fin 0), MemLp (f i) p μ), UnifTight f p μ
⊢ ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
have succ : ∀ (n : ℕ) (h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ) {f : Fin (n + 1) → α → β}
  (hf : ∀ (i : Fin (n + 1)), MemLp (f i) p μ), UnifTight f p μ
Tactic: induction n with
  | zero => exact fun {f} hf ↦ unifTight_of_subsingleton hp_top hf
  | succ n h =>
    intro f hfLp ε hε
    by_cases hε_top : ε = ∞
    · exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
    let g : Fin n → α → β := fun k => f k.castSucc
    have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
    obtain ⟨S, hμS, hFε⟩ := h hgLp hε
    obtain ⟨s, _, hμs, hfε⟩ :=
      (hfLp (Fin.last n)).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')
    refine ⟨s ∪ S, (by finiteness), fun i => ?_⟩
    by_cases! hi : i.val < n
    · rw [show f i = g ⟨i.val, hi⟩ from rfl, compl_union, ← indicator_indicator]
      apply (eLpNorm_indicator_le _).trans
      exact hFε (Fin.castLT i hi)
    · obtain rfl : i = Fin.last n := Fin.ext (le_antisymm i.is_le hi)
      rw [compl_union, inter_comm, ← indicator_indicator]
      exact (eLpNorm_indicator_le _).trans hfε.le
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have obtain : ∀ (n : ℕ) (hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have hg : ∀ (i : Fin n), MemLp (g i) p μ
Tactic: have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have obtain : ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨s, hμs, hfε⟩ := unifTight_fin hp_top hg hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have refine : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: refine ⟨s, hμs, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop (𝓝 0)
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have rw : ∀ (hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε) ⦃ε : ℝ≥0⦄ (hε : 0 < ε),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
Cleared hypotheses: hf_tendsto, ε, hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have obtain : ∀ (N : ℕ) (hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have hF : ∀ (n : Fin N), MemLp (F n) p μ
Tactic: have hF : ∀ n, MemLp (F n) p μ := fun n => hf n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
have obtain : ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)),
  ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: obtain ⟨s, hμs, hFε⟩ := unifTight_fin hp' hF hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), 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∞)
have refine : ∀ (n : ℕ), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: refine ⟨s, hμs, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
have pos : ∀ (hn : n < N), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: by_cases! hn : n < N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
pos : ∀ (hn : n < N), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
have neg : ∀ (hn : N ≤ n), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
Tactic: by_cases! hn : n < N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
have h : ∀ (n : ℕ), f n = HAdd.hAdd (α := ℕ → α → β) (β := (n : ℕ) → α → β) (fun (x : ℕ) ↦ g) (fun (n : ℕ) ↦ f n - g) n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ UnifTight f p μ
have this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
Tactic: have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight f p μ
have rw : UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ
have refine_1 : UnifTight.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ
Tactic: refine UnifTight.add ?_ ?_ (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
refine_1 : UnifTight.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ
⊢ UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ
have refine_2 : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ
Tactic: refine UnifTight.add ?_ ?_ (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos : ∀ (hfinε : ε ≠ ∞), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: by_cases hfinε : ε ≠ ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
pos : ∀ (hfinε : ε ≠ ∞), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have neg : ∀ (hfinε : ¬ε ≠ ∞), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: by_cases hfinε : ε ≠ ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have neg : ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ∞
Tactic: rw [not_ne_iff.mp hfinε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos : ∀ (hg' : MemLp (m0 := m) g p 0) (hui : @UnifIntegrable _ _ _ _ m f p 0) (hut : @UnifTight _ _ _ _ m f p 0)
  (hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
  ∃ (N : ℕ), ∀ n ≥ N, @eLpNorm _ _ _ m (f n - g) p 0 ≤ ε
Tactic: obtain rfl | hμ := eq_or_ne μ 0
Cleared hypotheses: μ, hg', hui, hut, hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
pos :
  ∀ (hg' : MemLp (m0 := m) g p 0) (hui : @UnifIntegrable _ _ _ _ m f p 0) (hut : @UnifTight _ _ _ _ m f p 0)
    (hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
    ∃ (N : ℕ), ∀ n ≥ N, @eLpNorm _ _ _ m (f n - g) p 0 ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos₁ : ∀ (hμ : μ ≠ 0), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: obtain rfl | hμ := eq_or_ne μ 0