-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞)
    (hf : ∀ i, MemLp (f i) p μ) : UniformIntegrable f p μ

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
refine ⟨C.toNNReal, fun i => ?_⟩

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑C.toNNReal

Proof state:
case pos.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i✝ i : ι
⊢ eLpNorm (f i) p μ < ⊤

Tactic:
exact hf i

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑C.toNNReal

Tactic:
rw [ENNReal.coe_toNNReal]

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ C

case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ C ≠ ⊤

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
by_cases hι : Nonempty ι

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
choose _ hf using hf

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
⊢ UniformIntegrable f p μ

Tactic:
refine ⟨fun n => (hf n).1, unifIntegrable_finite hp_one hp_top hf, ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ C ≠ ⊤

Tactic:
refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
y : ℝ≥0∞
hy : y ∈ Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ
⊢ y < ⊤

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
⊢ UniformIntegrable f p μ

Tactic:
cases nonempty_fintype ι

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
⊢ UniformIntegrable f p μ

Proof state:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
exact ⟨0, fun i => False.elim <| hι <| Nonempty.intro i⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
set C := (Finset.univ.image fun i : ι => eLpNorm (f i) p μ).max'
  ⟨eLpNorm (f hι.some) p μ, Finset.mem_image.2 ⟨hι.some, Finset.mem_univ _, rfl⟩⟩

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C