awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ)
⊢ Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b) f_lim) fi (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)
have simp_rw : Tendsto (β := ℝ)
    (fun (b : ι) ↦ (eLpNorm ((↑(↑(f b) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ).toReal) fi (𝓝 0) ↔
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ) fi
    (𝓝 0)
Tactic: simp_rw [dist_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ)
⊢ Tendsto (β := ℝ)
      (fun (b : ι) ↦ (eLpNorm ((↑(↑(f b) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ).toReal) fi
      (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)
have rw : ∀ (n : ι), eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
Tactic: rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
have rw : eLpNorm (↑(↑(f n - f_lim) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
Tactic: rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ
⊢ Tendsto f fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp)) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) fi (𝓝 0)
have 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)
Tactic: rw [tendsto_Lp_iff_tendsto_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ
⊢ 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)
have 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)
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ
⊢ 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)
have 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 μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 (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)
have rw : Tendsto (β := ℝ≥0∞)
    (fun (n : ι) ↦
      eLpNorm ((↑(↑(MemLp.toLp (f n) sorry) : α →ₘ[μ] 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: rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm' (fun n => (f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
have refine : ∀ (n : ι),
  eLpNorm ((↑(↑(MemLp.toLp (f n) sorry) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f n - f_lim) p μ
Tactic: refine Filter.tendsto_congr fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 : ι
⊢ eLpNorm ((↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f n - f_lim) p μ
have hfg : (↑(↑(MemLp.toLp (f n) sorry) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  f n - f_lim
Tactic: apply eLpNorm_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 : ι
⊢ (↑(↑(MemLp.toLp (f n) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    f n - f_lim
have h : ∀ (a : α) (hx₁ : (↑(↑(MemLp.toLp (f n - f_lim) sorry) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a)
  (hx₂ :
    (↑(↑(MemLp.toLp (f n) sorry - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a =
      ((↑(↑(MemLp.toLp (f n) sorry) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a),
  ((↑(↑(MemLp.toLp (f n) sorry) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a =
    (f n - f_lim) a
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₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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) ⋯) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E)) a =
    (f n - f_lim) a
have h : (↑(↑(MemLp.toLp (f n) sorry - MemLp.toLp f_lim f_lim_ℒp) : α →ₘ[μ] E) : α → E) a = (f n - f_lim) a
Tactic: rw [← hx₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ)
⊢ CauchySeq f ↔
    Tendsto (β := ℝ≥0∞)
      (fun (n : ι × ι) ↦ eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ) atTop
      (𝓝 0)
have 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)
Tactic: simp_rw [cauchySeq_iff_tendsto_dist_atTop_0, dist_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ)
⊢ 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)
have rw : ∀ (n : ι × ι), eLpNorm ((↑(↑(f n.1) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
Tactic: rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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) : α →ₘ[μ] E) : α → E) - (↑(↑(f n.2) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
have rw : eLpNorm (↑(↑(f n.1 - f n.2) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
Tactic: rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ CompleteSpace ↥(Lp E p μ)
have hB_pos : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 μ)
have 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)
Tactic: refine Metric.complete_of_convergent_controlled_sequences B hB_pos fun f hf => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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
⊢ ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)
have 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)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
⊢ ∃ (x : ↥(Lp E p μ)), Tendsto f atTop (𝓝 x)
have rsuffices₁ : ∃ (f_lim : α → E),
  MemLp f_lim p μ ∧
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
have 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)
Tactic: obtain ⟨M, hB⟩ : Summable B := summable_geometric_two
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 M
have rw : ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)
Tactic: rw [← hB.tsum_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)
have h_tsum_B1 : ∑' (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 (ENNReal.ofReal M)
have h_sum : HasSum B1 (∑' (b : ℕ), B1 b)
Tactic: have h_sum := (@ENNReal.summable _ B1).hasSum
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
⊢ HasSum B1 (ENNReal.ofReal M)
have rwa : ∀ (h_sum : HasSum B1 (ENNReal.ofReal M)), HasSum B1 (ENNReal.ofReal M)
Tactic: rwa [h_tsum_B1] at h_sum
Cleared hypotheses: h_sum
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
have hB1_has : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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) ∞
have rw : ENNReal.ofReal M < ∞
Tactic: rw [hB1_has.tsum_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
have hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
Tactic: have hB1 : ∑' i, B1 i < ∞ := by
    rw [hB1_has.tsum_eq]
    exact ENNReal.ofReal_lt_top