-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem denseRange_coeSimpleFuncNonnegToLpNonneg [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) :
    DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G) := fun g ↦ by
  borelize G
  rw [mem_closure_iff_seq_limit]
  have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)
  have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y }

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᶠ[ae μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯
hx_tendsto : Tendsto (fun n => eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun n => ↑(toLp (x n) ⋯)) atTop (𝓝 ↑g)
⊢ Tendsto (fun n => coeSimpleFuncNonnegToLpNonneg p μ G ⟨toLp (x n) ⋯, ⋯⟩) atTop (𝓝 g)

Tactic:
rw [tendsto_iff_dist_tendsto_zero] at this ⊢

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᶠ[ae μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯
hx_tendsto : Tendsto (fun n => eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b => dist ↑(toLp (x b) ⋯) ↑g) atTop (𝓝 0)
⊢ Tendsto (fun b => dist (coeSimpleFuncNonnegToLpNonneg p μ G ⟨toLp (x b) ⋯, ⋯⟩) g) atTop (𝓝 0)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

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, eq_self_iff_true, true_or,
    mem_setOf_eq, le_refl, and_self_iff]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᶠ[ae μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯
⊢ Tendsto (fun n => eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)

Tactic:
apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top

Result:
case hμ
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᶠ[ae μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯
⊢ ∀ᵐ (x : α) ∂μ, ↑↑↑g x ∈ closure ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})

case hi
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᶠ[ae μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯
⊢ eLpNorm (fun x => ↑↑↑g x - 0) p μ < ⊤

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Tactic:
have hx_memLp : ∀ n, MemLp (x n) p μ :=
  SimpleFunc.memLp_approxOn _ hg_memLp _ ⟨aestronglyMeasurable_const, by simp⟩

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
⊢ 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}

Tactic:
simp only [union_singleton, mem_inter_iff, mem_insert_iff, eq_self_iff_true, true_or,
  mem_setOf_eq, le_refl, and_self_iff]

Result:
no goals