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
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)
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:
simpa using ha
-- 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 ⋯
hi : eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x) p μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x - 0) p μ < ∞

Tactic:
simp_rw [sub_zero]

Premises used: sub_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)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
⊢ eLpNorm.{u_1, u_7} (ε := G) (fun (x : α) ↦ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) x) p μ < ∞

Tactic:
finiteness
-- 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 ⋯
⊢ 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
-- 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 ⋯
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)

Tactic:
⟨fun n =>
      (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memLp n), hx_nonneg_Lp n⟩,
      fun n => mem_range_self _, ?_⟩

Premises used: Set.mem_range_self, MeasureTheory.SimpleFunc.toLp, Subtype.mk, And.intro, Exists.intro, MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg
-- 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 ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
n :
  Tendsto
    (fun (n : ℕ) ↦
      coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x n).toLp ⋯) ⋯))
    atTop (𝓝 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)

Tactic:
refine
    ⟨fun n =>
      (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memLp n), hx_nonneg_Lp n⟩,
      fun n => mem_range_self _, ?_⟩
-- 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_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 μ)))
rw :
  ∀ (this : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (↑((x b).toLp ⋯) : ↥(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 ⋯) ⋯))
          g)
      atTop (𝓝 0)
⊢ Tendsto
    (fun (n : ℕ) ↦
      coeSimpleFuncNonnegToLpNonneg p μ G (Subtype.mk (p := fun (g : ↥(simpleFunc G p μ)) ↦ 0 ≤ g) ((x n).toLp ⋯) ⋯))
    atTop (𝓝 g)

Tactic:
rw [tendsto_iff_dist_tendsto_zero] at this ⊢

Premises used: tendsto_iff_dist_tendsto_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_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 (b : ℕ) ↦ dist (↑((x b).toLp ⋯) : ↥(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 ⋯) ⋯)) :
          ↥(Lp G p μ))
        (↑g : ↥(Lp G p μ)))
    atTop (𝓝 0)

Tactic:
this
-- 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_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 (b : ℕ) ↦ dist (↑((x b).toLp ⋯) : ↥(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 ⋯) ⋯)) :
          ↥(Lp G p μ))
        (↑g : ↥(Lp G p μ)))
    atTop (𝓝 0)

Tactic:
exact this
-- 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 ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
suffices : 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)

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
-- 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 ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
rw :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm ((↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G))
        p μ)
    atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑((x n).toLp ⋯) : ↥(Lp G p μ))) atTop (𝓝 (↑g : ↥(Lp G p μ)))

Tactic:
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']

Premises used: MeasureTheory.Lp.tendsto_Lp_iff_tendsto_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 ⋯
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)

Tactic:
Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto

Premises used: Filter.Tendsto.congr, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- 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 ⋯
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)
refine_2 : ∀ (n : ℕ), (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (↑(↑(↑g : ↥(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)

Tactic:
refine Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto

Premises used: Filter.Tendsto.congr, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- 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 ⋯
hx_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ eLpNorm ((⇑(x n) : (a : α) → G) - (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)) p μ) atTop (𝓝 0)
n : ℕ
refine_1 : (↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)
⊢ (⇑(x n) : (a : α) → G) =ᶠ[ae μ] (↑(↑(↑((x n).toLp ⋯) : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)

Tactic:
symm