-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_fin (hp_top : p ≠ ∞) {n : ℕ} {f : Fin n → α → β}
    (hf : ∀ i, MemLp (f i) p μ) : UnifTight f p μ

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
hi : ↑i < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
rw [(_ : f i = g ⟨i.val, hi⟩)]

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
hi : ↑i < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (g ⟨↑i, hi⟩)) p μ ≤ ↑ε

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
hi : ↑i < n
⊢ f i = g ⟨↑i, hi⟩

Proof state:
case neg.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
by_cases hi : i.val < n

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
hi : ↑i < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
hi : ¬↑i < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
⊢ ∀ {f : Fin (n + 1) → α → β}, (∀ (i : Fin (n + 1)), MemLp (f i) p μ) → UnifTight f p μ

Tactic:
intro f hfLp ε hε

Result:
case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
obtain ⟨S, hμS, hFε⟩ := h hgLp hε

Result:
case neg.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case neg.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
refine ⟨s ∪ S, (by measurability), fun i => ?_⟩

Result:
case neg.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (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 : ¬↑ε = ⊤
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ⊤
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε
i : Fin (n + 1)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε