-- 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:
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 => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

Tactic:
have h_rw_sum :
    (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x := by
  ext1 n
  change
    (∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i)) = f n x - f 0 x
  rw [Finset.sum_range_sub (fun m => f m x)]

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 => ∑ i ∈ Finset.range n, (f (i + 1) x - f i 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
⊢ ∃ 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
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)

Tactic:
obtain ⟨l, hx⟩ := hx

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 => ∑ 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
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)
⊢ (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x

Tactic:
ext1 n

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, (f (i + 1) x - f i x) = f n x - f 0 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 => ∑ 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

Tactic:
rw [Finset.sum_range_sub (fun m => f m x)]

Result:
no goals

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 : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

Tactic:
have h_summable : ∀ᵐ x ∂μ, Summable fun i : ℕ => f (i + 1) x - f i x := by
  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
  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)
  have h3 : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i :=
    lintegral_rpow_tsum_coe_enorm_sub_le_tsum hf hp1 h2
  have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
    tsum_enorm_sub_ae_lt_top hf hp1 hB h3
  exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne

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
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)