Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : 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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x ↦ x ^ p
h_rpow_surj : Function.Surjective fun y ↦ y ^ p
⊢ liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) atTop ^ p =
    liminf (fun n ↦ (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) ^ p) atTop

Tactic:
refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : 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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x ↦ x ^ p
h_rpow_surj : Function.Surjective fun y ↦ y ^ p
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

case refine_2
α : 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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x ↦ x ^ p
h_rpow_surj : Function.Surjective fun y ↦ y ^ p
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

case refine_3
α : 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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x ↦ x ^ p
h_rpow_surj : Function.Surjective fun y ↦ y ^ p
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x_1 ↦
    (StrictMono.orderIsoOfSurjective (fun x ↦ x ^ p) h_rpow_mono h_rpow_surj)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)

case refine_4
α : 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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x ↦ x ^ p
h_rpow_surj : Function.Surjective fun y ↦ y ^ p
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x_1 ↦
    (StrictMono.orderIsoOfSurjective (fun x ↦ x ^ p) h_rpow_mono h_rpow_surj)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)