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
g : α →ₛ G
hp : Membership.mem (γ := AddSubgroup (α →ₘ[μ] G)) (Lp G p μ) (AEEqFun.mk (⇑g : (a : α) → G) ⋯)
hf : EventuallyLE.{u_1, u_7} (β := G) (ae μ) 0 (⇑g : (a : α) → G)
refine_1 :
  ∀ (x : α),
    LE.le.{u_7} (α := G) ((0 : (a : α) → G) x : G)
      ((SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g : (a : α) → G) x : G)
⊢ ∃ (f' : α →ₛ G),
    0 ≤ f' ∧
      (↑(↑(↑(Subtype.mk (p := fun (x : ↥(Lp G p μ)) ↦
                      Membership.mem (γ := AddSubgroup ↥(Lp G p μ)) (simpleFunc G p μ) x)
                      (Subtype.mk (p := fun (x : α →ₘ[μ] G) ↦
                        Membership.mem (γ := AddSubgroup (α →ₘ[μ] G)) (Lp G p μ) x) (AEEqFun.mk (⇑g : (a : α) → G) ⋯)
                        hp)
                      ⋯) :
                  ↥(Lp G p μ)) :
              α →ₘ[μ] G) :
          α → G) =ᶠ[ae μ]
        (⇑f' : (a : α) → G)
have refine_2 : EventuallyEq.{u_1, u_7} (β := G) (ae μ) (⇑g : (a : α) → G)
  (⇑(SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g) : (a : α) → G)
Tactic: classical
  refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
  · simpa using Set.indicator_apply_nonneg id
  · filter_upwards [hf] with x (hx : 0 ≤ g x)
    simpa using Set.indicator_of_mem hx id |>.symm
-- 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 }
⊢ Membership.mem (γ := Set { g : ↥(Lp G p μ) // 0 ≤ g })
    (closure[instTopologicalSpaceSubtype] (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))) g
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ Membership.mem (γ := Set { g : ↥(Lp G p μ) // 0 ≤ g })
    (closure[instTopologicalSpaceSubtype] (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))) g
have rw : ∃ (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)
Tactic: rw [mem_closure_iff_seq_limit]
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ ∃ (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 hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
Tactic: have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
⊢ ∃ (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 zero_mem : 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}
Tactic: have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } := by
    simp only [union_singleton, mem_inter_iff, mem_insert_iff, true_or,
      mem_setOf_eq, le_refl, and_self_iff]
-- 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 : MeasurableSpace G := borel G
this_1 : 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}
⊢ SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
have hs : IsSeparable ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
Tactic: apply IsSeparable.separableSpace
-- 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 : MeasurableSpace G := borel G
this_1 : 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}
⊢ IsSeparable ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
have apply : IsSeparable (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0})
Tactic: apply IsSeparable.mono _ Set.inter_subset_left
-- 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 : MeasurableSpace G := borel G
this_1 : 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}
⊢ ∃ (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 this : SeparableSpace.{u_7} (↑((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}) : Type u_7)
Tactic: have : SeparableSpace ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y } : Set G) := by
    apply IsSeparable.separableSpace
    apply IsSeparable.mono _ Set.inter_subset_left
    exact
      (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
        (finite_singleton _).isSeparable
-- 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)
⊢ ∃ (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 g_meas : Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
Tactic: have g_meas : Measurable (g : α → G) := (Lp.stronglyMeasurable (g : Lp G p μ)).measurable
-- 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
n : ℕ
a : α
⊢ LE.le.{u_7} (α := G) ((0 : (a : α) → G) a : G) ((x n : (a : α) → G) a : G)
have change : Membership.mem.{u_7, u_7} (α := G) (γ := Set G) {y : G | 0 ≤ y} ((x n : (a : α) → G) a : G)
Tactic: change x n a ∈ { y : G | 0 ≤ y }
-- 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
n : ℕ
a : α
⊢ Membership.mem.{u_7, u_7} (α := G) (γ := Set G) {y : G | 0 ≤ y} ((x n : (a : α) → G) a : G)
have A : (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y} ⊆ {y : G | 0 ≤ y}
Tactic: have A : (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } ⊆ { y | 0 ≤ y } :=
      inter_subset_right
-- 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
n : ℕ
a : α
A : (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y} ⊆ {y : G | 0 ≤ y}
⊢ Membership.mem.{u_7, u_7} (α := G) (γ := Set G) {y : G | 0 ≤ y} ((x n : (a : α) → G) a : G)
have a₁ : Membership.mem (α := G) ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
  ((x n : (a : α) → G) a : G)
Tactic: apply A
-- 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
⊢ ∃ (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_nonneg : ∀ (n : ℕ), 0 ≤ x n
Tactic: have hx_nonneg : ∀ n, 0 ≤ x n := by
    intro n a
    change x n a ∈ { y : G | 0 ≤ y }
    have A : (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } ⊆ { y | 0 ≤ y } :=
      inter_subset_right
    apply A
    exact SimpleFunc.approxOn_mem g_meas _ n a
-- 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
⊢ ∃ (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_memLp : ∀ (n : ℕ), MemLp.{u_1, u_7} (ε := G) (⇑(x n) : (a : α) → G) p μ
Tactic: have hx_memLp : ∀ n, MemLp (x n) p μ :=
    SimpleFunc.memLp_approxOn _ hg_memLp _ ⟨aestronglyMeasurable_const, by simp⟩
-- 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 μ
⊢ ∃ (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 h_toLp : ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) sorry) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
Tactic: have h_toLp := fun n => MemLp.coeFn_toLp (hx_memLp n)
-- 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)
n : ℕ
⊢ 0 ≤ (x n).toLp ⋯
have rw : (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) sorry) : α →ₘ[μ] G) : α → G)
Tactic: rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
-- 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)
n : ℕ
⊢ (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G)
have h : ∀ (a : α) (ha0 : Eq.{u_7 + 1} (α := G) ((↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a) (0 a))
  (ha_toLp : (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) sorry) : α →ₘ[μ] G) : α → G) a = (x n : (a : α) → G) a),
  (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a ≤ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) sorry) : α →ₘ[μ] G) : α → G) a
Tactic: filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
-- 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)
n : ℕ
a : α
ha0 : Eq.{u_7 + 1} (α := G) ((↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a) (0 a)
ha_toLp : (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) a = (x n : (a : α) → G) a
⊢ (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a ≤ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) a
have h : LE.le.{u_7} (α := G) (0 a : G) ((x n : (a : α) → G) a : G)
Tactic: rw [ha0, ha_toLp]
-- 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)
⊢ ∃ (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_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp sorry
Tactic: have hx_nonneg_Lp : ∀ n, 0 ≤ toLp (x n) (hx_memLp n) := by
    intro n
    rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
    filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
    rw [ha0, ha_toLp]
    exact hx_nonneg n a
-- 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 ⋯
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
have 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})
Tactic: apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top