-- 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 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 μ ≤ ↑ε

Tactic:
by_cases hε_top : ε = ∞

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 : ↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (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 : ¬↑ε = ⊤
⊢ ∃ 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 : 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 [(_ : i = n)]

Result:
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 ↑n)) 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
⊢ i = ↑n

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ᶜ.indicator (g ⟨↑i, hi⟩)) p μ ≤ ↑ε

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

Result:
no goals

Proof state:
α : 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) ≠ ⊤

Tactic:
measurability

Result:
no goals

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 : ↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
exact ⟨∅, (by measurability), fun _ => hε_top.symm ▸ le_top⟩

Result:
no goals

Proof state:
α : 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
hi' : ↑i < n + 1
⊢ i = ↑n

Tactic:
rw [Nat.lt_succ_iff] at hi'

Result:
α : 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
hi' : ↑i ≤ n
⊢ i = ↑n

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 (g ⟨↑i, hi⟩)) p μ ≤ ↑ε

Tactic:
rw [compl_union, ← indicator_indicator]

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ᶜ.indicator (Sᶜ.indicator (g ⟨↑i, hi⟩))) p μ ≤ ↑ε