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

Tactic:
rw [Lp.simpleFunc.toLp_eq_toLp]

Premises used: MeasureTheory.Lp.simpleFunc.toLp_eq_toLp
-- 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 : ℕ
⊢ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)

Tactic:
h_toLp n
-- 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 : ℕ
⊢ (↑(↑(MemLp.toLp (⇑(x n) : (a : α) → G) ⋯) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (⇑(x n) : (a : α) → G)

Tactic:
exact h_toLp n
-- 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 : ℕ
⊢ (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp G p μ)) : α →ₘ[μ] G) : α → G)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)), motive f

Tactic:
fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f isClosed ?_

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, DenseRange.induction_on
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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}
refine : ∀ (f : ↥(Lp E p μ)) (a : ↥(simpleFunc E p μ)), motive (↑a : ↥(Lp E p μ))
⊢ ∀ (f : ↥(Lp E p μ)), motive f

Tactic:
refine fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f isClosed ?_
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
⊢ ∀ (a : ↥(simpleFunc E p μ)), motive (↑a : ↥(Lp E p μ))

Tactic:
Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne'
    hp_ne_top ?_ ?_

Premises used: LT.lt.ne', zero_lt_one, Fact.elim, lt_of_lt_of_le, MeasureTheory.Lp.simpleFunc.induction
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ))
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 μ))
⊢ ∀ (a : ↥(simpleFunc E p μ)), motive (↑a : ↥(Lp E p μ))

Tactic:
refine Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne'
    hp_ne_top ?_ ?_
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
⊢ ∀ (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 μ))

Tactic:
fun c s => indicatorConst c
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
⊢ ∀ (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 μ))

Tactic:
exact fun c s => indicatorConst c
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
⊢ ∀ ⦃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:
fun f g hf hg => add hf hg

Premises used: Set.Mem, MeasureTheory.MemLp.toLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
⊢ ∀ ⦃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:
exact fun f g hf hg => add hf hg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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)
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)
⊢ ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)

Tactic:
apply SimpleFunc.induction
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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)
neg : ∀ (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)

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
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)
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
subst hc
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
    μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
    μ
h₁ :
  Eq (α := α → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
convert! indicator 0 MeasurableSet.empty (by simp) using 1

Premises used: MeasurableSet.empty, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
    μ
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)
⊢ Eq (α := α → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
    μ
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:
simp