-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_of_tendsto_Lp (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ)
    (hg : MemLp g p μ) (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)) :
    UnifIntegrable f p μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable (fun x => g) p μ

Tactic:
exact unifIntegrable_const hp hp' hg

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
n : ℕ
⊢ f n = ((fun x => g) + fun n => f n - g) n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ UnifIntegrable f p μ

Tactic:
have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable f p μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable ((fun x => g) + fun n => f n - g) p μ

Tactic:
refine UnifIntegrable.add ?_ ?_ hp (fun _ => hg.aestronglyMeasurable)
    fun n => (hf n).1.sub hg.aestronglyMeasurable

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable (fun x => g) p μ

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable (fun n => f n - g) p μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ f = (fun x => g) + fun n => f n - g

Tactic:
ext1 n

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
n : ℕ
⊢ f n = ((fun x => g) + fun n => f n - g) n

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable (fun n => f n - g) p μ

Tactic:
exact unifIntegrable_of_tendsto_Lp_zero hp hp' (fun n => (hf n).sub hg) hfg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable f p μ

Tactic:
rw [this]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x => g) + fun n => f n - g
⊢ UnifIntegrable ((fun x => g) + fun n => f n - g) p μ