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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : ↥(Lp E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    motive (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p μ))
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (support f) (support g) →
      motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)
isClosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive f}
f : ↥(Lp E p μ)
refine_1 :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    motive (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p μ))
⊢ ∀ (a : ↥(simpleFunc E p μ)), motive (↑a : ↥(Lp E p μ))
have refine_2 : ∀ ⦃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)) →
    motive (↑(f.toLp hf) : ↥(Lp E p μ)) →
      motive (↑(g.toLp hg) : ↥(Lp E p μ)) → motive (↑(f.toLp hf + g.toLp hg) : ↥(Lp E p μ))
Tactic: refine Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne'
    hp_ne_top ?_ ?_
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
have const : ∀ (c : E) {s : Set α} (hs : MeasurableSet s),
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
      μ →
    motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
Tactic: apply SimpleFunc.induction
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
const :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s),
    MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
        p μ →
      motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
⊢ ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
have add₁ : ∀ ⦃f g : α →ₛ E⦄,
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
      (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
    (MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)) →
      (MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ → motive (⇑g : (a : α) → E)) →
        MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ → motive (⇑(f + g) : (a : α) → E)
Tactic: apply SimpleFunc.induction
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
have pos : ∀ (hc : c = 0), motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
pos : ∀ (hc : c = 0), motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
have neg : ∀ (hc : ¬c = 0), motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
have pos : ∀
  (h :
    MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
      p μ),
  motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
Tactic: subst hc
Cleared hypotheses: c, h, hc
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
have h₁ : Eq (α := α → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
  (Set.indicator ∅ fun (x : α) ↦ 0)
Tactic: convert! indicator 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
⊢ Eq (α := α → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)
have h₁ : ∀ (x : α),
  Eq.{u_4 + 1} (α := E) ((SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → E) x : E)
    (Set.indicator ∅ (fun (x : α) ↦ 0) x : E)
Tactic: ext
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
have neg : ∀ (hp_pos : p ≠ 0), motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
Tactic: have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
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 : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ → motive (⇑g : (a : α) → E)
int_fg : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
⊢ motive (⇑(f + g) : (a : α) → E)
have int_fg₁ : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
Tactic: rw [SimpleFunc.coe_add,
        memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
Cleared hypotheses: int_fg
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → motive f
have this : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
Tactic: have : ∀ f : SimpleFunc α E, MemLp f p μ → motive f := by
    apply SimpleFunc.induction
    · intro c s hs h
      by_cases hc : c = 0
      · subst hc; convert! indicator 0 MeasurableSet.empty (by simp) using 1; ext; simp
      have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
      exact indicator c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)
    · intro f g hfg hf hg int_fg
      rw [SimpleFunc.coe_add,
        memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
      exact add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)
-- 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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → motive f
have this₁ : ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
Tactic: have : ∀ f : Lp.simpleFunc E p μ, motive f := by
    intro f
    exact
      ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
        (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this_1 : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
this : ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → motive f
have this₁ : ∀ (f : ↥(Lp E p μ)), motive (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: have : ∀ f : Lp E p μ, motive f := fun f =>
    (Lp.simpleFunc.denseRange hp_ne_top).induction_on f closed this
-- 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_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have inl : ∀ (hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞)
  (h0P :
    ∀ (c : E) ⦃s : Set α⦄,
      MeasurableSet s →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) 0 μ ≤ ε ∧ P g)
  (hf : MemLp f 0 μ), ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
Tactic: rcases eq_or_ne p 0 with (rfl | hp_pos)
Cleared hypotheses: p, hp_ne_top, h0P, hf
-- 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_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞)
    (h0P :
      ∀ (c : E) ⦃s : Set α⦄,
        MeasurableSet s →
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
            ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) 0 μ ≤ ε ∧ P g)
    (hf : MemLp f 0 μ), ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have inr : ∀ (hp_pos : p ≠ 0), ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
Tactic: rcases eq_or_ne p 0 with (rfl | hp_pos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
⊢ ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
have inl : ∀ (g : α → E),
  eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) 0 μ ≤ ε → ∀ (Pg : P g), ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
Tactic: rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
        hε with ⟨g, _, Pg⟩
-- 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_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have obtain : ∀ (η : ℝ≥0∞) (ηpos : 0 < η)
  (hη :
    ∀ (f g : α → E),
      AEStronglyMeasurable f μ →
        AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε),
  ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
Tactic: obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε
-- 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_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have rcases : ∀ (f' : α →ₛ E) (hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η)
  (f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ), ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
Tactic: rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩
-- 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_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have rcases : ∀ (g : α → E) (hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η) (Pg : P g), ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
Tactic: rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩