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

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h1 : ∀ (n : ℕ), eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x

Tactic:
have h2 n :
    ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p :=
  lintegral_rpow_sum_enorm_sub_le_rpow_tsum hp1 n (h1 n)

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h1 : ∀ (n : ℕ), eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
l : E
hx : Tendsto (fun n => f n x - f 0 x) atTop (𝓝 l)
h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x
hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x
⊢ ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

Tactic:
rw [hf_rw]

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
l : E
hx : Tendsto (fun n => f n x - f 0 x) atTop (𝓝 l)
h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x
hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x
⊢ ∃ l, Tendsto (fun n => f n x - f 0 x + f 0 x) atTop (𝓝 l)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

Tactic:
refine h.mono fun x hx => ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
hx : ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x

Tactic:
have h1 :
  ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
  eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h1 : ∀ (n : ℕ), eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
l : E
hx : Tendsto (fun n => f n x - f 0 x) atTop (𝓝 l)
h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x
n : ℕ
⊢ f n x = f n x - f 0 x + f 0 x

Tactic:
abel

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
l : E
hx : Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
n : ℕ
⊢ ∑ i ∈ Finset.range n, (f (i + 1) x - f i x) = f n x - f 0 x

Tactic:
change
  (∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i)) = f n x - f 0 x

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x
h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
x : α
l : E
hx : Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
n : ℕ
⊢ ∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i) = f n x - f 0 x