awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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}
a₁ :
  Membership.mem (α := G) ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
    ((x n : (a : α) → G) a : G)
⊢ Membership.mem.{u_7, u_7} (α := G) (γ := Set G) {y : G | 0 ≤ y} ((x n : (a : α) → G) a : G)

Tactic:
apply A
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 (α := G) ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
    ((x n : (a : α) → G) a : G)

Tactic:
SimpleFunc.approxOn_mem g_meas _ n a

Premises used: Set.Mem, MeasureTheory.SimpleFunc.approxOn_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 (α := G) ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})
    ((x n : (a : α) → G) a : G)

Tactic:
exact SimpleFunc.approxOn_mem g_meas _ n a

Premises used: MeasureTheory.SimpleFunc.approxOn_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 : ℕ), 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
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
⊢ eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ 0) p μ < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
⊢ ∀ (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⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ
⊢ ∀ (n : ℕ), (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)

Tactic:
have h_toLp := fun n => MemLp.coeFn_toLp (hx_memLp n)
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 : ℕ
rw :
  (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G)
⊢ 0 ≤ (x n).toLp ⋯

Tactic:
rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]

Premises used: MeasureTheory.Lp.simpleFunc.toLp_eq_toLp, MeasureTheory.Lp.simpleFunc.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 : ℕ
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) ⋯) : α →ₘ[μ] G) : α → G) a = (x n : (a : α) → G) a),
    (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a ≤ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) a
⊢ (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G)

Tactic:
filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp

Premises used: MeasureTheory.Lp.simpleFunc.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
h : LE.le.{u_7} (α := G) (0 a : G) ((x n : (a : α) → G) a : G)
⊢ (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) a ≤ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) a

Tactic:
rw [ha0, ha_toLp]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
⊢ LE.le.{u_7} (α := G) (0 a : G) ((x n : (a : α) → G) a : G)

Tactic:
hx_nonneg n a
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
⊢ LE.le.{u_7} (α := G) (0 a : G) ((x n : (a : α) → G) a : G)

Tactic:
exact hx_nonneg n a
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 ⋯

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
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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})
hi : eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x - 0) p μ < ∞
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)

Tactic:
apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 ⋯
⊢ 0 ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)

Tactic:
have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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})

Tactic:
hg_nonneg.mono fun a ha => subset_closure ?_

Premises used: subset_closure, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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)
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}
⊢ ∀ᵐ (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:
refine hg_nonneg.mono fun a ha => subset_closure ?_

Premises used: subset_closure, Filter.Eventually.mono