awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have h_tsum_1 : ∀ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have 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
Tactic: simp_rw [h_tsum_1 _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), B i) atTop) p
have 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
Tactic: rw [← h_tsum_1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 ∂μ
have 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
Tactic: refine lintegral_congr fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)
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
have h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
Tactic: have h_rpow_mono := ENNReal.strictMono_rpow_of_pos (zero_lt_one.trans_le hp1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
⊢ 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
have h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
Tactic: have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ 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
have refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i 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
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
refine_2 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i 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
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
  (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
    (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
refine_2 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i 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
have refine_4 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
  (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
    (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have h_liminf_pow : ∫⁻ (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: have h_liminf_pow :
    ∫⁻ a, (atTop.liminf fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ =
      ∫⁻ a, atTop.liminf fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ := by
    refine lintegral_congr fun x => ?_
    have h_rpow_mono := ENNReal.strictMono_rpow_of_pos (zero_lt_one.trans_le hp1)
    have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
    refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
    all_goals isBoundedDefault
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
h_liminf_pow :
  ∫⁻ (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 ∂μ
⊢ ∫⁻ (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
have rw : ∫⁻ (a : α),
    liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ ≤
  HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: rw [h_liminf_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
h_liminf_pow :
  ∫⁻ (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 ∂μ
⊢ ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have refine : ∀ (n : ℕ),
  AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p)
    μ
Tactic: refine (lintegral_liminf_le' fun n ↦ ?_).trans <| liminf_le_of_frequently_le' <| .of_forall h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
have h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
Tactic: have h_tsum_lt_top : (∑' i, B i) ^ p < ∞ := ENNReal.rpow_lt_top_of_nonneg hp_pos.le hB
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
have refine : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤ HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: refine lt_of_le_of_lt ?_ h_tsum_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have rwa : ∀ (h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i)
  (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h
Cleared hypotheses: h, hp_pos, h_tsum_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
rwa :
  ∀ (h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (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 ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have rwa₁ : ∀
  (h :
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p⁻¹⁻¹)
  (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h
Cleared hypotheses: h, hp_pos, h_tsum_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
rwa :
  ∀ (h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
rwa₁ :
  ∀
    (h :
      ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
        HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p⁻¹⁻¹)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (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 ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have rwa₂ : ∀
  (h :
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p)
  (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h
Cleared hypotheses: h, hp_pos, h_tsum_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
have h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
Tactic: have h_integral : ∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ < ∞ := by
    have h_tsum_lt_top : (∑' i, B i) ^ p < ∞ := ENNReal.rpow_lt_top_of_nonneg hp_pos.le hB
    refine lt_of_le_of_lt ?_ h_tsum_lt_top
    rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
⊢ ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
have refine : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) μ
Tactic: refine ae_lt_top' (AEMeasurable.pow_const ?_ _) h_integral.ne