-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem cauchy_complete_eLpNorm [CompleteSpace E] (hp : 1 ≤ p) {f : ℕ → α → E}
    (hf : ∀ n, MemLp (f n) p μ) {B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞)
    (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) :
    ∃ (f_lim : α → E), MemLp f_lim p μ ∧
      atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
have h_ℒp_lim : MemLp f_lim p μ :=
  memLp_of_cauchy_tendsto hp hf f_lim h_f_lim_meas.aestronglyMeasurable h_tendsto'

Result:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
h_ℒp_lim : MemLp f_lim p μ
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨f_lim, h_f_lim_meas, h_lim⟩ :
    ∃ f_lim : α → E, StronglyMeasurable f_lim ∧
      ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x)) :=
  exists_stronglyMeasurable_limit_of_tendsto_ae (fun n => (hf n).1)
    (ae_tendsto_of_cauchy_eLpNorm (fun n => (hf n).1) hp hB h_cau)

Result:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
h_ℒp_lim : MemLp f_lim p μ
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
exact ⟨f_lim, h_ℒp_lim, h_tendsto'⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
have h_tendsto' : atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) :=
  cauchy_tendsto_of_tendsto (fun m => (hf m).1) f_lim hB h_cau h_lim

Result:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)