awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
hι : Nonempty ι
pos :
  ∀ (i : ι),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

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

Tactic:
obtain ⟨s, _, hμs, hfε⟩ := (hf i).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
i : ι
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : 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:
⟨s, ne_of_lt hμs, fun j => ?_⟩

Premises used: And.intro, Exists.intro, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
i : ι
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f i)) p μ < (↑ε : ℝ≥0∞)
pos : ∀ (j : ι), eLpNorm (sᶜ.indicator (f j)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
refine ⟨s, ne_of_lt hμs, fun j => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
i : ι
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f i)) p μ < (↑ε : ℝ≥0∞)
j : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
hfε.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬(↑ε : ℝ≥0∞) = ∞
i : ι
s : Set α
left : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : eLpNorm (sᶜ.indicator (f i)) p μ < (↑ε : ℝ≥0∞)
j : ι
⊢ eLpNorm (sᶜ.indicator (f j)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
convert! hfε.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ
revert : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifTight f p μ
⊢ UnifTight f p μ

Tactic:
revert f
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
⊢ ∀ {f : Fin 0 → α → β} (hf : ∀ (i : Fin 0), MemLp (f i) p μ), UnifTight f p μ

Tactic:
fun {f} hf ↦ unifTight_of_subsingleton hp_top hf

Premises used: MeasureTheory.unifTight_of_subsingleton
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
⊢ ∀ {f : Fin 0 → α → β} (hf : ∀ (i : Fin 0), MemLp (f i) p μ), UnifTight f p μ

Tactic:
exact fun {f} hf ↦ unifTight_of_subsingleton hp_top hf

Premises used: MeasureTheory.unifTight_of_subsingleton
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 < ε
pos :
  ∀ (hε_top : (↑ε : ℝ≥0∞) = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
neg :
  ∀ (hε_top : ¬(↑ε : ℝ≥0∞) = ∞),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
by_cases hε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞) = ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞) = ∞
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
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
⊢ ∀ (i : Fin n), MemLp (g i) p μ

Tactic:
have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ
neg :
  ∀ (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 : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨S, hμS, hFε⟩ := h hgLp hε
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
neg :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
        (hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < (↑ε : ℝ≥0∞)),
        ∃ (s : Set α),
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
            ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨s, _, hμs, hfε⟩ :=
      (hfLp (Fin.last n)).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', Fin.last, MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ S) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
neg : ∀ (i : Fin (n + 1)), eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
refine ⟨s ∪ S, (by finiteness), fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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∞)
neg : ∀ (hi : n ≤ (↑i : ℕ)), eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
by_cases! hi : i.val < n

Premises used: Fin.val
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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
pos : eLpNorm (sᶜ.indicator (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n)))) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
rw [show f i = g ⟨i.val, hi⟩ from rfl, compl_union, ← indicator_indicator]

Premises used: Set.compl_union, Set.indicator_indicator, rfl
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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
pos : eLpNorm (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n))) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm (sᶜ.indicator (Sᶜ.indicator (g (⟨(↑i : ℕ), hi⟩ : Fin n)))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
apply (eLpNorm_indicator_le _).trans

Premises used: MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (g (⟨(↑i : ℕ), hi⟩ : Fin n))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
hFε (Fin.castLT i hi)

Premises used: Fin.castLT
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 (g (⟨(↑i : ℕ), hi⟩ : Fin n))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact hFε (Fin.castLT i hi)

Premises used: Fin.castLT
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : ℕ)
⊢ i = Fin.last n

Tactic:
Fin.ext (le_antisymm i.is_le hi)

Premises used: Fin.is_le, Fin.ext, le_antisymm
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 : ℕ)
neg : ∀ (hi : n ≤ (↑(Fin.last n) : ℕ)), eLpNorm ((s ∪ S)ᶜ.indicator (f (Fin.last n))) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain rfl : i = Fin.last n := Fin.ext (le_antisymm i.is_le hi)

Premises used: Fin.ext, le_antisymm, Fin.last, rfl
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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) : ℕ)
neg : eLpNorm (Sᶜ.indicator (sᶜ.indicator (f (Fin.last n)))) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f (Fin.last n))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
rw [compl_union, inter_comm, ← indicator_indicator]

Premises used: Set.compl_union, Set.inter_comm, Set.indicator_indicator
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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ᶜ.indicator (sᶜ.indicator (f (Fin.last n)))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
(eLpNorm_indicator_le _).trans hfε.le

Premises used: LT.lt.le, MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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ᶜ.indicator (sᶜ.indicator (f (Fin.last n)))) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
exact (eLpNorm_indicator_le _).trans hfε.le

Premises used: LT.lt.le, MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
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 μ
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 μ
⊢ ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), 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

Premises used: Set.compl_union, Set.inter_comm, MeasureTheory.eLpNorm_indicator_le, Fin.last, Set.indicator_indicator, LE.le.trans, MeasureTheory.unifTight_of_subsingleton, rfl