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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
rw : ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal M

Tactic:
rw [← hB.tsum_eq]

Premises used: HasSum.tsum_eq
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)

Tactic:
(ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm

Premises used: le_of_lt, ENNReal.ofReal_tsum_of_nonneg, HasSum.summable, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)

Tactic:
exact (ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm

Premises used: le_of_lt, ENNReal.ofReal_tsum_of_nonneg, HasSum.summable, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
⊢ ∑' (i : ℕ), B1 i = ENNReal.ofReal M

Tactic:
have h_tsum_B1 : ∑' i, B1 i = ENNReal.ofReal M := by
      change (∑' n : ℕ, ENNReal.ofReal (B n)) = ENNReal.ofReal M
      rw [← hB.tsum_eq]
      exact (ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
h_tsum_B1 : ∑' (i : ℕ), B1 i = ENNReal.ofReal M
⊢ HasSum B1 (∑' (b : ℕ), B1 b)

Tactic:
have h_sum := (@ENNReal.summable _ B1).hasSum
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
h_tsum_B1 : ∑' (i : ℕ), B1 i = ENNReal.ofReal M
h_sum : HasSum B1 (∑' (b : ℕ), B1 b)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_sum : HasSum B1 (ENNReal.ofReal M)), HasSum B1 (ENNReal.ofReal M)
⊢ HasSum B1 (ENNReal.ofReal M)

Tactic:
rwa [h_tsum_B1] at h_sum
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
⊢ HasSum B1 (ENNReal.ofReal M)

Tactic:
have hB1_has : HasSum B1 (ENNReal.ofReal M) := by
    have h_tsum_B1 : ∑' i, B1 i = ENNReal.ofReal M := by
      change (∑' n : ℕ, ENNReal.ofReal (B n)) = ENNReal.ofReal M
      rw [← hB.tsum_eq]
      exact (ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm
    have h_sum := (@ENNReal.summable _ B1).hasSum
    rwa [h_tsum_B1] at h_sum
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
rw : ENNReal.ofReal M < ∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞

Tactic:
rw [hB1_has.tsum_eq]

Premises used: HasSum.tsum_eq
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ENNReal.ofReal M < ∞

Tactic:
ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ENNReal.ofReal M < ∞

Tactic:
exact ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞

Tactic:
have hB1 : ∑' i, B1 i < ∞ := by
    rw [hB1_has.tsum_eq]
    exact ENNReal.ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)

Tactic:
H f1 (fun n => Lp.memLp (f n)) B1 hB1 fun N n m hn hm => ?_

Premises used: MeasureTheory.Lp.memLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
refine : ∀ (N n m_1 : ℕ) (hn : N ≤ n) (hm : N ≤ m_1), eLpNorm (f1 n - f1 m_1) p μ < B1 N
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)

Tactic:
refine H f1 (fun n => Lp.memLp (f n)) B1 hB1 fun N n m hn hm => ?_

Premises used: MeasureTheory.Lp.memLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ dist (f n) (f m) < B N

Tactic:
specialize hf 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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : dist (f n) (f m) < B N
⊢ (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N

Tactic:
rw [dist_def] at hf

Premises used: MeasureTheory.Lp.dist_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
dsimp : eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ < B1 N
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N

Tactic:
dsimp only [f1]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
rwa : eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
⊢ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ < B1 N

Tactic:
rwa [ENNReal.lt_ofReal_iff_toReal_lt]

Premises used: ENNReal.lt_ofReal_iff_toReal_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
rw : eLpNorm (↑(↑(f n - f m) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
⊢ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞

Tactic:
rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]

Premises used: MeasureTheory.Lp.coeFn_sub, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m_1 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
⊢ eLpNorm (↑(↑(f n - f m) : α →ₘ[μ] E) : α → E) p μ ≠ ∞

Tactic:
Lp.eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
⊢ eLpNorm (↑(↑(f n - f m) : α →ₘ[μ] E) : α → E) p μ ≠ ∞

Tactic:
exact Lp.eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_ne_top
-- 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_1 : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
n : ℕ
x : α
⊢ Eq (α := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) ((∑ i ∈ Finset.range (n + 1), f_norm_diff i) x)

Tactic:
simp [f_norm_diff]
-- 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‖
⊢ ∀ (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)

Tactic:
have hgf_norm_diff :
    ∀ n,
      (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) =
        ∑ i ∈ Finset.range (n + 1), f_norm_diff i :=
    fun n => funext fun x => by simp [f_norm_diff]
-- 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)
rw : eLpNorm' (ε := ℝ) (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
rw [hgf_norm_diff]
-- 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)
⊢ eLpNorm' (ε := ℝ) (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i

Tactic:
(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