awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
refine :
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖(f (i + 1) - f i) x‖) p μ)
    (∑' (i : ℕ), B i)
⊢ eLpNorm' (ε := ℝ) (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i

Tactic:
refine (eLpNorm'_sum_le (fun i _ => ((hf (i + 1)).sub (hf i)).norm) hp1).trans ?_

Premises used: MeasureTheory.eLpNorm'_sum_le, MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.AEStronglyMeasurable.norm, HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
simp_rw : LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ) (∑' (i : ℕ), B i)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖(f (i + 1) - f i) x‖) p μ)
    (∑' (i : ℕ), B i)

Tactic:
simp_rw [eLpNorm'_norm]

Premises used: MeasureTheory.eLpNorm'_norm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ) (∑' (i : ℕ), B i)

Tactic:
(Finset.sum_le_sum ?_).trans <| ENNReal.sum_le_tsum _

Premises used: ENNReal.sum_le_tsum, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
refine : ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ) (∑' (i : ℕ), B i)

Tactic:
refine (Finset.sum_le_sum ?_).trans <| ENNReal.sum_le_tsum _

Premises used: ENNReal.sum_le_tsum, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i

Tactic:
fun m _ => (h_cau m (m + 1) m (Nat.le_succ m) (le_refl m)).le

Premises used: le_refl, LT.lt.le, Nat.le_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i

Tactic:
exact fun m _ => (h_cau m (m + 1) m (Nat.le_succ m) (le_refl m)).le

Premises used: le_refl, LT.lt.le, Nat.le_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ 0 < p

Tactic:
have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
rw :
  (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

Tactic:
rw [← inv_inv p, @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [hp_pos]), inv_inv p]

Premises used: ENNReal.le_rpow_inv_iff, inv_inv
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Tactic:
simp_rw [eLpNorm'_eq_lintegral_enorm, one_div] at hn

Premises used: one_div, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
h :
  ∀ (a : α),
    enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p =
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p

Tactic:
ext1 a
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
h :
  enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) =
    ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ
⊢ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p =
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
h :
  ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
⊢ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) =
    ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ

Tactic:
simp_rw [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
h :
  ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
h₁ : ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖
⊢ ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖

Tactic:
rw [← ENNReal.ofReal_sum_of_nonneg]

Premises used: ENNReal.ofReal_sum_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
rw : LE.le (α := ℝ) 0 (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
⊢ ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)

Tactic:
rw [Real.norm_of_nonneg _]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)

Tactic:
Finset.sum_nonneg fun x _ => norm_nonneg _

Premises used: HSub.hSub, Finset.sum_nonneg, HAdd.hAdd, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)

Tactic:
exact Finset.sum_nonneg fun x _ => norm_nonneg _

Premises used: Finset.sum_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖

Tactic:
fun x _ => norm_nonneg _

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖

Tactic:
exact fun x _ => norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p

Tactic:
have h_nnnorm_nonneg :
    (fun a => ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a =>
      (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p := by
    ext1 a
    congr
    simp_rw [← ofReal_norm]
    rw [← ENNReal.ofReal_sum_of_nonneg]
    · rw [Real.norm_of_nonneg _]
      exact Finset.sum_nonneg fun x _ => norm_nonneg _
    · exact fun x _ => norm_nonneg _
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
h_nnnorm_nonneg :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hn :
      (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤
        ∑' (i : ℕ), B i)
    (h_nnnorm_nonneg :
      Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
        (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
        HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p),
    (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤
      ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Tactic:
rwa [h_nnnorm_nonneg] at hn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ 0 < p

Tactic:
have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_pow :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_pow :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
rwa : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
rwa₁ :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p⁻¹⁻¹
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i

Tactic:
rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]

Premises used: ENNReal.le_rpow_inv_iff, inv_inv, one_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
suffices :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i

Tactic:
suffices h_pow : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ≤ (∑' i, B i) ^ p by
      rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
rw :
  Eq (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, g i) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∑ i ∈ Finset.range (i + 1), g i) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)

Tactic:
rw [ENNReal.tsum_eq_liminf_sum_nat, ← liminf_nat_add _ 1]

Premises used: ENNReal.tsum_eq_liminf_sum_nat, Filter.liminf_nat_add, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
⊢ ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)

Tactic:
have h_tsum_1 :
    ∀ g : ℕ → ℝ≥0∞, ∑' i, g i = atTop.liminf fun n => ∑ i ∈ Finset.range (n + 1), g i := by
    intro g
    rw [ENNReal.tsum_eq_liminf_sum_nat, ← liminf_nat_add _ 1]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
simp_rw :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), B i) atTop) p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

Tactic:
simp_rw [h_tsum_1 _]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
rw :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), B i) atTop) p

Tactic:
rw [← h_tsum_1]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
⊢ ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ

Tactic:
lintegral_congr fun x => ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
refine :
  ∀ (x : α),
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) atTop) p =
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) p) atTop
⊢ ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ

Tactic:
refine lintegral_congr fun x => ?_

Premises used: MeasureTheory.lintegral_congr