-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem memLp_of_cauchy_tendsto (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ n, MemLp (f n) p μ)
    (f_lim : α → E) (h_lim_meas : AEStronglyMeasurable f_lim μ)
    (h_tendsto : atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)) : MemLp f_lim p μ

Proof state:
case intro.right
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f N) p μ < ⊤

Tactic:
exact (hf N).2

Result:
no goals

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm f_lim p μ < ⊤

Tactic:
rw [h_add]

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N + f N) p μ < ⊤

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ⊤

Tactic:
specialize h_tendsto_1 N (le_refl N)

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ MemLp f_lim p μ

Tactic:
refine ⟨h_lim_meas, ?_⟩

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ eLpNorm f_lim p μ < ⊤

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ + eLpNorm (f N) p μ < ⊤

Tactic:
rw [ENNReal.add_lt_top]

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ⊤ ∧ eLpNorm (f N) p μ < ⊤

Proof state:
case intro.left
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ ≤ 1

Tactic:
have h_neg : f_lim - f N = -(f N - f_lim) := by simp

Result:
case intro.left
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (f_lim - f N) p μ ≤ 1

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
⊢ f_lim = f_lim - f N + f N

Tactic:
abel

Result:
no goals

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ⊤

Tactic:
have h_add : f_lim = f_lim - f N + f N := by abel

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm f_lim p μ < ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ eLpNorm f_lim p μ < ⊤

Tactic:
rw [ENNReal.tendsto_atTop_zero] at h_tendsto

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
⊢ eLpNorm f_lim p μ < ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ f_lim - f N = -(f N - f_lim)

Tactic:
simp

Result:
no goals

Proof state:
case intro.left
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (f_lim - f N) p μ ≤ 1

Tactic:
rwa [h_neg, eLpNorm_neg]

Result:
no goals