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

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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 α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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 h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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 α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight ((fun x => g) + fun n => f n - g) p μ

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

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight (fun x => g) p μ

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight (fun n => f n - g) p μ

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight (fun n => f n - g) p μ

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

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight (fun x => g) p μ

Tactic:
exact unifTight_const hp' hg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight f p μ

Tactic:
rw [this]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
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
⊢ UnifTight ((fun x => g) + fun n => f n - g) p μ

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