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
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑(↑(f n - f_lim) : α →ₘ[μ] 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 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑(↑(f n - f_lim) : α →ₘ[μ] 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 α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
rw :
  Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)
⊢ Tendsto f fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp)) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [tendsto_Lp_iff_tendsto_eLpNorm']

Premises used: MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
h_eq :
  Eq.{u_4 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦
      eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
    fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ
rw rw₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
suffices :
  Eq.{u_4 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦
      eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
    fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ
⊢ Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)

Tactic:
suffices h_eq :
      (fun n => eLpNorm (⇑(f n) - ⇑(MemLp.toLp f_lim f_lim_ℒp)) p μ) =
        (fun n => eLpNorm (⇑(f n) - f_lim) p μ) by
    rw [h_eq]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Eq.{u_4 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦
      eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
    fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ

Tactic:
funext fun n => eLpNorm_congr_ae (EventuallyEq.rfl.sub (MemLp.coeFn_toLp f_lim_ℒp))

Premises used: funext, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.rfl, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Eq.{u_4 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦
      eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ)
    fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ

Tactic:
exact funext fun n => eLpNorm_congr_ae (EventuallyEq.rfl.sub (MemLp.coeFn_toLp f_lim_ℒp))

Premises used: funext, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.rfl, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
rw :
  Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E))
          p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - f_lim) p μ) fi (𝓝 0)
⊢ Tendsto (fun (n : ι) ↦ MemLp.toLp (f n) ⋯) fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp)) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm' (fun n => (f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)]

Premises used: MeasureTheory.MemLp.toLp, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E))
          p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
Filter.tendsto_congr fun n => ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
refine :
  ∀ (n : ι),
    eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p
        μ =
      eLpNorm (f n - f_lim) p μ
⊢ Tendsto (β := ℝ≥0∞)
      (fun (n : ι) ↦
        eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E))
          p μ)
      fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
refine Filter.tendsto_congr fun n => ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
hfg :
  (↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    f n - f_lim
⊢ eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f n - f_lim) p μ

Tactic:
apply eLpNorm_congr_ae

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
h :
  ∀ (a : α) (hx₁ : (↑(↑(MemLp.toLp (f n - f_lim) ⋯) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a)
    (hx₂ :
      (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a =
        ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a),
    ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a =
      (f n - f_lim) a
⊢ (↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    f n - f_lim

Tactic:
filter_upwards [((f_ℒp n).sub f_lim_ℒp).coeFn_toLp,
    Lp.coeFn_sub ((f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)] with _ hx₁ hx₂

Premises used: MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.Lp.coeFn_sub, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a : α
hx₁ : (↑(↑(MemLp.toLp (f n - f_lim) ⋯) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a
hx₂ :
  (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a =
    ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a
h : (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a
⊢ ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a =
    (f n - f_lim) a

Tactic:
rw [← hx₂]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a : α
hx₁ : (↑(↑(MemLp.toLp (f n - f_lim) ⋯) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a
hx₂ :
  (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a =
    ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a
⊢ (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a

Tactic:
hx₁

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.comp₂, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a : α
hx₁ : (↑(↑(MemLp.toLp (f n - f_lim) ⋯) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a
hx₂ :
  (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a =
    ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a
⊢ (↑(↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a

Tactic:
exact hx₁
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)
⊢ Tendsto f fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp))

Tactic:
(tendsto_Lp_iff_tendsto_eLpNorm f f_lim f_lim_ℒp).mpr h_tendsto

Premises used: Iff.mpr, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
simp_rw :
  Tendsto (β := ℝ)
      (fun (n : ι × ι) ↦ (eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ).toReal)
      atTop (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞)
      (fun (n : ι × ι) ↦ eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ) atTop
      (𝓝 0)
⊢ CauchySeq f ↔
    Tendsto (β := ℝ≥0∞)
      (fun (n : ι × ι) ↦ eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ) atTop
      (𝓝 0)

Tactic:
simp_rw [cauchySeq_iff_tendsto_dist_atTop_0, dist_def]

Premises used: MeasureTheory.Lp.dist_def, cauchySeq_iff_tendsto_dist_atTop_0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
rw : ∀ (n : ι × ι), eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
⊢ Tendsto (β := ℝ)
      (fun (n : ι × ι) ↦ (eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ).toReal)
      atTop (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞)
      (fun (n : ι × ι) ↦ eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ) atTop
      (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

Premises used: ENNReal.zero_ne_top, ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
rw : eLpNorm (↑(↑(f n.1 - f n.2) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
⊢ eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] 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 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑(↑(f n.1 - f n.2) : α →ₘ[μ] E) : α → E) p μ ≠ ∞

Tactic:
eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑(↑(f n.1 - f n.2) : α →ₘ[μ] E) : α → E) p μ ≠ ∞

Tactic:
exact eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_ne_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
⊢ ∀ (n : ℕ), 0 < B n

Tactic:
have hB_pos : ∀ n, 0 < B n := fun n => pow_pos (div_pos zero_lt_one zero_lt_two) n
-- 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
⊢ CompleteSpace ↥(Lp E p μ)

Tactic:
Metric.complete_of_convergent_controlled_sequences B hB_pos fun f hf => ?_

Premises used: Metric.complete_of_convergent_controlled_sequences
-- 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
refine :
  ∀ (f : ℕ → ↥(Lp E p μ)) (hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N),
    ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)
⊢ CompleteSpace ↥(Lp E p μ)

Tactic:
refine Metric.complete_of_convergent_controlled_sequences B hB_pos fun f hf => ?_

Premises used: Metric.complete_of_convergent_controlled_sequences
-- 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
rsuffices :
  ∀ (f_lim : α → E) (hf_lim_meas : MemLp f_lim p μ)
    (h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)),
    ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)
rsuffices₁ :
  ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)

Tactic:
rsuffices ⟨f_lim, hf_lim_meas, h_tendsto⟩ :
    ∃ (f_lim : α → E), MemLp f_lim p μ ∧
      atTop.Tendsto (fun n => eLpNorm (⇑(f n) - f_lim) p μ) (𝓝 0)
-- 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
f_lim : α → E
hf_lim_meas : MemLp f_lim p μ
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)

Tactic:
⟨hf_lim_meas.toLp f_lim, tendsto_Lp_of_tendsto_eLpNorm f_lim hf_lim_meas h_tendsto⟩

Premises used: MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm, MeasureTheory.MemLp.toLp, Exists.intro
-- 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
f_lim : α → E
hf_lim_meas : MemLp f_lim p μ
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)

Tactic:
exact ⟨hf_lim_meas.toLp f_lim, tendsto_Lp_of_tendsto_eLpNorm f_lim hf_lim_meas h_tendsto⟩
-- 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
⊢ Summable B

Tactic:
summable_geometric_two

Premises used: summable_geometric_two
-- 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
obtain :
  ∀ (M : ℝ) (hB : HasSum B M),
    ∃ (f_lim : α → E),
      MemLp f_lim p μ ∧
        Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨M, hB⟩ : Summable B := summable_geometric_two

Premises used: summable_geometric_two, Summable, SummationFilter.unconditional
-- 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)
change : ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal M
⊢ ∑' (i : ℕ), B1 i = ENNReal.ofReal M

Tactic:
change (∑' n : ℕ, ENNReal.ofReal (B n)) = ENNReal.ofReal M

Premises used: ENNReal.ofReal, tsum, SummationFilter.unconditional