awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hμ :
  ∀ᵐ (x : α) ∂μ,
    (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
have hi : eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x - 0) p μ < ∞
Tactic: apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
⊢ ∀ᵐ (x : α) ∂μ,
    (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
have hg_nonneg : 0 ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
Tactic: have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hg_nonneg : 0 ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
⊢ ∀ᵐ (x : α) ∂μ,
    (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
have hμ : ∀ (a : α) (ha : 0 a ≤ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a),
  (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a ∈
    (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
Tactic: refine hg_nonneg.mono fun a ha => subset_closure ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
⊢ eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x - 0) p μ < ∞
have hi : eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x) p μ < ∞
Tactic: simp_rw [sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
⊢ ∃ (x : ℕ → { g : ↥(Lp G p μ) // 0 ≤ g }),
    (∀ (n : ℕ),
        Membership.mem (γ := Set { g : ↥(Lp G p μ) // 0 ≤ g }) (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))
          (x n)) ∧
      Tendsto x atTop (𝓝 g)
have hx_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ)
  atTop (𝓝 0)
Tactic: have hx_tendsto :
      Tendsto (fun n : ℕ => eLpNorm ((x n : α → G) - (g : α → G)) p μ) atTop (𝓝 0) := by
    apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top
    · have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
      refine hg_nonneg.mono fun a ha => subset_closure ?_
      simpa using ha
    · simp_rw [sub_zero]; finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
⊢ ∃ (x : ℕ → { g : ↥(Lp G p μ) // 0 ≤ g }),
    (∀ (n : ℕ),
        Membership.mem (γ := Set { g : ↥(Lp G p μ) // 0 ≤ g }) (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))
          (x n)) ∧
      Tendsto x atTop (𝓝 g)
have n : Tendsto
  (fun (n : ℕ) ↦
    coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x n).toLp sorry) sorry))
  atTop (𝓝 g)
Tactic: refine
    ⟨fun n =>
      (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memLp n), hx_nonneg_Lp n⟩,
      fun n => mem_range_self _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this_3 :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
this : Tendsto (fun (n : ℕ) ↦ (↑((x n).toLp ⋯) : ↥(Lp G p μ))) atTop (𝓝 (↑g : ↥(Lp G p μ)))
⊢ Tendsto
    (fun (n : ℕ) ↦
      coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x n).toLp ⋯) ⋯))
    atTop (𝓝 g)
have rw : ∀ (this : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (↑((x b).toLp sorry) : ↥(Lp G p μ)) (↑g : ↥(Lp G p μ))) atTop (𝓝 0)),
  Tendsto (β := ℝ)
    (fun (b : ℕ) ↦
      dist
        (coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x b).toLp sorry) sorry))
        g)
    atTop (𝓝 0)
Tactic: rw [tendsto_iff_dist_tendsto_zero] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
⊢ Tendsto
    (fun (n : ℕ) ↦
      coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x n).toLp ⋯) ⋯))
    atTop (𝓝 g)
have suffices : Tendsto (fun (n : ℕ) ↦ (↑((x n).toLp sorry) : ↥(Lp G p μ))) atTop (𝓝 (↑g : ↥(Lp G p μ)))
Tactic: suffices Tendsto (fun n : ℕ => (toLp (x n) (hx_memLp n) : Lp G p μ)) atTop (𝓝 (g : Lp G p μ)) by
    rw [tendsto_iff_dist_tendsto_zero] at this ⊢
    simp_rw [Subtype.dist_eq]
    exact this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑((x n).toLp ⋯) : ↥(Lp G p μ))) atTop (𝓝 (↑g : ↥(Lp G p μ)))
have rw : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    eLpNorm ((↑(↑(↑((x n).toLp sorry) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p
      μ)
  atTop (𝓝 0)
Tactic: rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm ((↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G))
        p μ)
    atTop (𝓝 0)
have refine_1 : ∀ (n : ℕ), (⇑(x n) : (a : α) → G) =ᶠ[ae μ] (↑(↑(↑((x n).toLp sorry) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
Tactic: refine Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
refine_1 : ∀ (n : ℕ), (⇑(x n) : (a : α) → G) =ᶠ[ae μ] (↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm ((↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G))
        p μ)
    atTop (𝓝 0)
have refine_2 : ∀ (n : ℕ), (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
Tactic: refine Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
n : ℕ
⊢ (⇑(x n) : (a : α) → G) =ᶠ[ae μ] (↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
have refine_1 : (↑(↑(↑((x n).toLp sorry) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
inst_2 : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g : ↥(Lp G p μ) // 0 ≤ g }
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
this :
  SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
x : (n : ℕ) → α →ₛ G :=
  fun (n : ℕ) ↦
    approxOn (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) g_meas
      ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
n : ℕ
⊢ (↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
have refine_1 : (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) sorry) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
Tactic: rw [Lp.simpleFunc.toLp_eq_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : ↥(Lp E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    motive (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p μ))
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (support f) (support g) →
      motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)
isClosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive f}
⊢ ∀ (f : ↥(Lp E p μ)), motive f
have refine : ∀ (f : ↥(Lp E p μ)) (a : ↥(simpleFunc E p μ)), motive (↑a : ↥(Lp E p μ))
Tactic: refine fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f isClosed ?_