awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
pos : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N
pos₁ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (B n).toReal) atTop (𝓝 0)
⊢ CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ f n x

Tactic:
refine cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) ?_ ?_

Premises used: cauchySeq_of_le_tendsto_0, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
⊢ ‖(f n - f m) x‖ₑ < B N

Tactic:
specialize hx N n m hnN hmN
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ‖(f n - f m) x‖ₑ < B N
pos : ‖f n x - f m x‖ₑ ≤ B N
⊢ dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N

Tactic:
rw [_root_.dist_eq_norm,
        ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.ne_top_of_tsum_ne_top hB N),
        ofReal_norm]

Premises used: dist_eq_norm, ENNReal.ofReal_le_iff_le_toReal, ofReal_norm, ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ‖(f n - f m) x‖ₑ < B N
⊢ ‖f n x - f m x‖ₑ ≤ B N

Tactic:
hx.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ‖(f n - f m) x‖ₑ < B N
⊢ ‖f n x - f m x‖ₑ ≤ B N

Tactic:
exact hx.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ Tendsto (fun (n : ℕ) ↦ (B n).toReal) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
Tendsto.comp (g := ENNReal.toReal) (ENNReal.tendsto_toReal ENNReal.zero_ne_top)
          (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, ENNReal.tendsto_atTop_zero_of_tsum_ne_top, ENNReal.toReal, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ Tendsto (fun (n : ℕ) ↦ (B n).toReal) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
exact
        Tendsto.comp (g := ENNReal.toReal) (ENNReal.tendsto_toReal ENNReal.zero_ne_top)
          (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, ENNReal.tendsto_atTop_zero_of_tsum_ne_top, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
rw : 1 ≤ p
⊢ 1 ≤ p.toReal

Tactic:
rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]

Premises used: ENNReal.ofReal_le_iff_le_toReal, ENNReal.ofReal_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
⊢ 1 ≤ p

Tactic:
hp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
⊢ 1 ≤ p

Tactic:
exact hp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
⊢ 1 ≤ p.toReal

Tactic:
have hp1 : 1 ≤ p.toReal := by
    rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]
    exact hp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm (f n - f m) p μ < B N

Tactic:
specialize h_cau N n m hn hm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
h_cau : eLpNorm (f n - f m) p μ < B N
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_cau : eLpNorm' (f n - f m) p.toReal μ < B N), eLpNorm' (f n - f m) p.toReal μ < B N
⊢ eLpNorm' (f n - f m) p.toReal μ < B N

Tactic:
rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', Ne.symm, zero_lt_one, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
⊢ ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N

Tactic:
have h_cau' : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p.toReal μ < B N := by
    intro N n m hn hm
    specialize h_cau N n m hn hm
    rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
h_cau' : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
ae_tendsto_of_cauchy_eLpNorm' hf hp1 hB h_cau'

Premises used: MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
h_cau' : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
exact ae_tendsto_of_cauchy_eLpNorm' hf hp1 hB h_cau'

Premises used: MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
rw [ENNReal.tendsto_atTop_zero]

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
suffices : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → B n ≤ ε
⊢ ∃ (N : ℕ), B N ≤ ε

Tactic:
suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → B n ≤ ε

Tactic:
(ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε

Premises used: ENNReal.tendsto_atTop_zero_of_tsum_ne_top, Iff.mp, ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → B n ≤ ε

Tactic:
exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε

Premises used: ENNReal.tendsto_atTop_zero_of_tsum_ne_top, Iff.mp, ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), B N ≤ ε

Tactic:
have h_B : ∃ N : ℕ, B N ≤ ε := by
    suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
    exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_B : ∃ (N : ℕ), B N ≤ ε
obtain : ∀ (N : ℕ) (h_B : B N ≤ ε), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
obtain ⟨N, h_B⟩ := h_B
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
⟨N, fun n hn => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
refine : ∀ (n : ℕ) (hn : n ≥ N), eLpNorm (f n - f_lim) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
refine ⟨N, fun n hn => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop

Tactic:
eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_

Premises used: MeasureTheory.AEStronglyMeasurable.sub, HSub.hSub, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
refine : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
⊢ eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop

Tactic:
refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_

Premises used: MeasureTheory.AEStronglyMeasurable.sub, HSub.hSub, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))

Tactic:
h_lim.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
refine :
  ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))),
    Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
simp_rw : Tendsto (fun (n_1 : ℕ) ↦ (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))
⊢ Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun (n_1 : ℕ) ↦ (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))

Tactic:
Tendsto.add tendsto_const_nhds (Tendsto.neg hx)

Premises used: Filter.Tendsto.neg, tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun (n_1 : ℕ) ↦ (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))

Tactic:
exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)

Premises used: Filter.Tendsto.neg, tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop

Tactic:
have h_sub : eLpNorm (f n - f_lim) p μ ≤ atTop.liminf fun m => eLpNorm (f n - f m) p μ := by
    refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_
    refine h_lim.mono fun x hx => ?_
    simp_rw [sub_eq_add_neg]
    exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
⊢ eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
h_sub.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
refine : liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop ≤ ε
⊢ eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
refine h_sub.trans ?_

Premises used: LE.le.trans