awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
pos : ∀ (hc : c = 0), P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
have neg : ∀ (hc : ¬c = 0), P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
have h : (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf =
  simpleFunc.indicatorConst p (s := ∅) sorry sorry 0
Tactic: convert! indicatorConst 0 MeasurableSet.empty (by simp) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
⊢ (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf =
    simpleFunc.indicatorConst p (s := ∅) ⋯ ⋯ 0
have h : (↑((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf) : ↥(Lp E p μ)) =
  (↑(simpleFunc.indicatorConst p (s := ∅) sorry sorry 0) : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
hfg :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E))
hf : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
⊢ P ((f + g).toLp hfg')
have hf' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
      (memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
hfg :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E))
hf : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
hf' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ P ((f + g).toLp hfg')
have hg' : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
Tactic: obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
      (memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 ≠ ∞
⊢ IsDenseEmbedding (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ IsDenseEmbedding (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))
have apply : 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: apply simpleFunc.isUniformEmbedding.isDenseEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.range (ι := ↥(simpleFunc E p μ))
        (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
          Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))))
    f
have rw : ∃ (x : ℕ → ↥(Lp E p μ)),
  (∀ (n : ℕ),
      Membership.mem (γ := Set ↥(Lp E p μ))
        (Set.range (ι := ↥(simpleFunc E p μ))
          (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
            Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
        (x n)) ∧
    Tendsto x atTop (𝓝 f)
Tactic: rw [mem_closure_iff_seq_limit]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
⊢ ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)
have hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
Tactic: have hfi' : MemLp f p μ := Lp.memLp f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
⊢ ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)
have this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
Tactic: haveI : SeparableSpace (range f ∪ {0} : Set E) :=
    (Lp.stronglyMeasurable f).separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)
have n : Tendsto
  (fun (n : ℕ) ↦
    (↑((approxOn (↑(↑f : α →ₘ[μ] E) : α → E) sorry (Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) 0 sorry n).toLp sorry) :
      ↥(Lp E p μ)))
  atTop (𝓝 f)
Tactic: refine
    ⟨fun n =>
      toLp
        (SimpleFunc.approxOn f (Lp.stronglyMeasurable f).measurable (range f ∪ {0}) 0 _ n)
        (SimpleFunc.memLp_approxOn_range (Lp.stronglyMeasurable f).measurable hfi' n),
      fun n => mem_range_self _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑((approxOn (↑(↑f : α →ₘ[μ] E) : α → E) ⋯ (Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) 0 ⋯ n).toLp ⋯) :
        ↥(Lp E p μ)))
    atTop (𝓝 f)
have h : f = MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hfi'
Tactic: convert! SimpleFunc.tendsto_approxOn_range_Lp hp_ne_top (Lp.stronglyMeasurable f).measurable hfi'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ f = MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hfi'
have h : f = f
Tactic: rw [toLp_coeFn f (Lp.memLp f)]
-- 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
f g : ↥(simpleFunc G p μ)
⊢ (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ f ≤ g
have rw : (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔
  (↑f : ↥(Lp G p μ)) ≤ (↑g : ↥(Lp G p μ))
Tactic: rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]
-- 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
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 μ))
⊢ (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ≤ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ f ≤ g
have 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)
Tactic: rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]
-- 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
f : ↥(simpleFunc G p μ)
⊢ 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ 0 ≤ f
have rw : 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ (↑0 : ↥(Lp G p μ)) ≤ (↑f : ↥(Lp G p μ))
Tactic: rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]
-- 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
f : ↥(simpleFunc G p μ)
rw : 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ (↑0 : ↥(Lp G p μ)) ≤ (↑f : ↥(Lp G p μ))
⊢ 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ 0 ≤ f
have rw₁ : 0 ≤ (↑f : ↥(Lp G p μ)) ↔ (↑0 : ↥(Lp G p μ)) ≤ (↑f : ↥(Lp G p μ))
Tactic: rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]
-- 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
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 μ))
⊢ 0 ≤ᶠ[ae μ] (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) ↔ 0 ≤ f
have rw₂ : 0 ≤ (↑f : ↥(Lp G p μ)) ↔ 0 ≤ (↑f : ↥(Lp G p μ))
Tactic: rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]
-- 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
f : ↥(simpleFunc G p μ)
hf : 0 ≤ f
⊢ ∃ (f' : α →ₛ G), 0 ≤ f' ∧ (↑(↑(↑f : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑f' : (a : α) → G)
have rcases : ∀ (g : α →ₛ G) (hp : Membership.mem (γ := AddSubgroup (α →ₘ[μ] G)) (Lp G p μ) (AEEqFun.mk (⇑g : (a : α) → G) sorry))
  (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) sorry) hp)
        sorry)),
  ∃ (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) sorry)
                        hp)
                      sorry) :
                  ↥(Lp G p μ)) :
              α →ₘ[μ] G) :
          α → G) =ᶠ[ae μ]
        (⇑f' : (a : α) → G)
Tactic: rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩
Cleared hypotheses: f, hf
-- 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
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)
have hf₁ : EventuallyLE.{u_1, u_7} (β := G) (ae μ) 0 (⇑g : (a : α) → G)
Tactic: change 0 ≤ᵐ[μ] g at hf
Cleared hypotheses: hf
-- 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)
⊢ ∃ (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_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)
Tactic: refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
-- 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: refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
-- 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)
x : α
⊢ 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)
have 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)
Tactic: (hx : 0 ≤ g x)
-- 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)
⊢ 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)
have 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)
Tactic: filter_upwards [hf] with x (hx : 0 ≤ g x)
-- 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)
⊢ ∃ (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_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)
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