awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
h : f = MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hfi'
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑((approxOn (↑(↑f : α →ₘ[μ] E) : α → E) ⋯ (Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) 0 ⋯ n).toLp ⋯) :
        ↥(Lp E p μ)))
    atTop (𝓝 f)

Tactic:
convert! SimpleFunc.tendsto_approxOn_range_Lp hp_ne_top (Lp.stronglyMeasurable f).measurable hfi'

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
h h₁ : f = f
⊢ f = MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hfi'

Tactic:
rw [toLp_coeFn f (Lp.memLp f)]

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.Lp.toLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
⊢ IsDenseInducing (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
(simpleFunc.isDenseEmbedding hp_ne_top).isDenseInducing

Premises used: IsDenseEmbedding.isDenseInducing, MeasureTheory.Lp.simpleFunc.isDenseEmbedding
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
⊢ DenseRange (X := ↥(Lp E p μ)) (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
(simpleFunc.isDenseInducing hp_ne_top).dense

Premises used: IsDenseInducing.dense, MeasureTheory.Lp.simpleFunc.isDenseInducing
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
⊢ Dense (↑(simpleFunc E p μ) : Set ↥(Lp E p μ))

Tactic:
simpa only [denseRange_subtype_val] using simpleFunc.denseRange (E := E) (μ := μ) hp_ne_top

Premises used: denseRange_subtype_val, MeasureTheory.Lp.simpleFunc.denseRange
-- 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
f g : ↥(simpleFunc G p μ)
rw :
  (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔
    (↑f : ↥(Lp G p μ)) ≤ (↑g : ↥(Lp G p μ))
rw₁ rw₂ :
  (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔
    (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ f ≤ g

Tactic:
rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]

Premises used: Subtype.coe_le_coe, MeasureTheory.Lp.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
inst : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst_1 : NormedAddCommGroup G
⊢ EventuallyEq.{u_1, u_7} (β := G) (ae μ) (↑(↑(↑0 : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) 0

Tactic:
Lp.coeFn_zero _ _ _

Premises used: MeasureTheory.Lp.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
f : ↥(simpleFunc G p μ)
rw : 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ (↑0 : ↥(Lp G p μ)) ≤ (↑f : ↥(Lp G p μ))
rw₁ : 0 ≤ (↑f : ↥(Lp G p μ)) ↔ (↑0 : ↥(Lp G p μ)) ≤ (↑f : ↥(Lp G p μ))
rw₂ rw₃ : 0 ≤ (↑f : ↥(Lp G p μ)) ↔ 0 ≤ (↑f : ↥(Lp G p μ))
⊢ 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ 0 ≤ f

Tactic:
rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]

Premises used: Subtype.coe_le_coe, MeasureTheory.Lp.coeFn_nonneg, AddSubmonoid.coe_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
f : ↥(simpleFunc G p μ)
hf : 0 ≤ f
rcases :
  ∀ (g : α →ₛ G) (hp : Membership.mem (γ := AddSubgroup (α →ₘ[μ] G)) (Lp G p μ) (AEEqFun.mk (⇑g : (a : α) → G) ⋯))
    (hf :
      LE.le (α := ↥(simpleFunc G p μ)) 0
        (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)
          ⋯)),
    ∃ (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)
⊢ ∃ (f' : α →ₛ G), 0 ≤ f' ∧ (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑f' : (a : α) → G)

Tactic:
rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩

Premises used: rfl
-- 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
g : α →ₛ G
hp : Membership.mem (γ := AddSubgroup (α →ₘ[μ] G)) (Lp G p μ) (AEEqFun.mk (⇑g : (a : α) → G) ⋯)
hf :
  LE.le (α := ↥(simpleFunc G p μ)) 0
    (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)
      ⋯)
⊢ EventuallyLE.{u_1, u_7} (β := G) (ae μ) 0 (⇑g : (a : α) → G)

Tactic:
change 0 ≤ᵐ[μ] g at hf
-- 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
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)
⊢ ∃ (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)

Tactic:
⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩

Premises used: Filter.EventuallyEq.trans, setOf, id, MeasureTheory.AEEqFun.coeFn_mk, LE.le, And.intro, Exists.intro, Set.piecewise, OfNat.ofNat, MeasureTheory.SimpleFunc.map
-- 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
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)
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)
⊢ ∃ (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)

Tactic:
refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
-- 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
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)
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)

Tactic:
simpa using Set.indicator_apply_nonneg id

Premises used: Set.indicator_apply_nonneg
-- 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
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)
x : α
h :
  ∀ (hx : LE.le.{u_7} (α := G) (0 : G) ((g : (a : α) → G) x : G)),
    Eq.{u_7 + 1} (α := G) ((g : (a : α) → G) x : G)
      ((SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g : (a : α) → G) x : G)
⊢ LE.le.{u_7} (α := G) (0 x : G) ((g : (a : α) → G) x : G) →
    Eq.{u_7 + 1} (α := G) ((g : (a : α) → G) x : G)
      ((SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g : (a : α) → G) x : G)

Tactic:
(hx : 0 ≤ g x)
-- 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
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)
h :
  ∀ (x : α) (hx : LE.le.{u_7} (α := G) (0 : G) ((g : (a : α) → G) x : G)),
    Eq.{u_7 + 1} (α := G) ((g : (a : α) → G) x : G)
      ((SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g : (a : α) → G) x : G)
⊢ 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:
filter_upwards [hf] with x (hx : 0 ≤ g x)
-- 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
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)
x : α
hx : LE.le.{u_7} (α := G) (0 : G) ((g : (a : α) → G) x : G)
⊢ Eq.{u_7 + 1} (α := G) ((g : (a : α) → G) x : G)
    ((SimpleFunc.map (Set.piecewise (β := fun (a : G) ↦ G) {x : G | 0 ≤ x} id 0) g : (a : α) → G) x : G)

Tactic:
simpa using Set.indicator_of_mem hx id |>.symm

Premises used: id, Set.indicator_of_mem, Eq.symm
-- 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
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)
refine_2 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)
⊢ ∃ (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)

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

Premises used: Set.indicator_apply_nonneg
-- 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 }
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
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)
⊢ Membership.mem (γ := Set { g : ↥(Lp G p μ) // 0 ≤ g })
    (closure[instTopologicalSpaceSubtype] (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))) g

Tactic:
rw [mem_closure_iff_seq_limit]

Premises used: mem_closure_iff_seq_limit
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ

Tactic:
have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
⊢ 0 ∈ (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y}

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

Premises used: le_refl, true_or, Set.mem_inter_iff, Set.mem_setOf_eq, and_self_iff, Set.mem_insert_iff, Set.union_singleton
-- 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 : MeasurableSpace G := borel G
this_1 : BorelSpace G
hg_memLp : MemLp (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) p μ
⊢ 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]
-- 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 : 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}
hs : IsSeparable ((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)

Tactic:
apply IsSeparable.separableSpace

Premises used: TopologicalSpace.IsSeparable.separableSpace
-- 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 : 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}
apply : IsSeparable (Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0})
⊢ IsSeparable ((Set.range (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ∪ {0}) ∩ {y : G | 0 ≤ y})

Tactic:
apply IsSeparable.mono _ Set.inter_subset_left

Premises used: Set.inter_subset_left, TopologicalSpace.IsSeparable.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 : 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})

Tactic:
(Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
        (finite_singleton _).isSeparable

Premises used: MeasureTheory.StronglyMeasurable.isSeparable_range, MeasureTheory.Lp.stronglyMeasurable, Set.Finite.isSeparable, Subtype.val, Set.finite_singleton, TopologicalSpace.IsSeparable.union
-- 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 : 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})

Tactic:
exact
      (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
        (finite_singleton _).isSeparable

Premises used: MeasureTheory.StronglyMeasurable.isSeparable_range, MeasureTheory.Lp.stronglyMeasurable, Set.Finite.isSeparable, Subtype.val, Set.finite_singleton, TopologicalSpace.IsSeparable.union
-- 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 : 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)

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
-- 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)
⊢ Measurable (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)

Tactic:
have g_meas : Measurable (g : α → G) := (Lp.stronglyMeasurable (g : Lp G p μ)).measurable
-- 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 : α
change : Membership.mem.{u_7, u_7} (α := G) (γ := Set G) {y : G | 0 ≤ y} ((x n : (a : α) → G) a : G)
⊢ LE.le.{u_7} (α := G) ((0 : (a : α) → G) a : G) ((x n : (a : α) → G) a : G)

Tactic:
change x n a ∈ { y : G | 0 ≤ y }

Premises used: DFunLike.coe
-- 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 : α
⊢ (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