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
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : p = ∞
pos : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) ∞ μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
rw [hp_top]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) ∞ μ

Tactic:
memLp_top f μ

Premises used: MeasureTheory.SimpleFunc.memLp_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) ∞ μ

Tactic:
exact memLp_top f μ

Premises used: MeasureTheory.SimpleFunc.memLp_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
⟨f.aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.MemLp, And.intro, MeasureTheory.SimpleFunc.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg : eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
refine ⟨f.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg :
  HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞))
      (1 / p.toReal) <
    ∞
⊢ eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', MeasureTheory.SimpleFunc.eLpNorm'_eq
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ 0 ≤ 1 / p.toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg :
  ∀ y ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
      ∞
⊢ HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞))
      (1 / p.toReal) <
    ∞

Tactic:
refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne

Premises used: Iff.mpr, ENNReal.sum_lt_top, ENNReal.rpow_lt_top_of_nonneg, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
pos :
  ∀ (hy0 : y = 0),
    HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
      ∞
neg :
  ∀ (hy0 : ¬y = 0),
    HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
      ∞
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞

Tactic:
by_cases hy0 : y = 0
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
hy0 : y = 0
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞

Tactic:
simp [hy0, ENNReal.toReal_pos hp0 hp_top]

Premises used: ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
hy0 : ¬y = 0
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞

Tactic:
ENNReal.mul_lt_top ?_ (hf y hy0)

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
hy0 : ¬y = 0
neg : ‖y‖ₑ ^ p.toReal < ∞
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞

Tactic:
refine ENNReal.mul_lt_top ?_ (hf y hy0)

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal < ∞

Tactic:
ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top

Premises used: ENNReal.toReal_nonneg, ENNReal.rpow_lt_top_of_nonneg, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
h : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top

Premises used: ENNReal.toReal_nonneg, ENNReal.rpow_lt_top_of_nonneg, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ↔
    ∀ (y : E),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨fun h => measure_preimage_lt_top_of_memLp hp_pos hp_ne_top f h, fun h =>
    memLp_of_finite_measure_preimage p h⟩

Premises used: MeasureTheory.SimpleFunc.memLp_of_finite_measure_preimage, MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
⊢ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ ↔
    ∀ (y : E),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
memLp_one_iff_integrable.symm.trans <| memLp_iff one_ne_zero ENNReal.coe_ne_top

Premises used: MeasureTheory.SimpleFunc.memLp_iff, Iff.trans, one_ne_zero, MeasureTheory.memLp_one_iff_integrable, Iff.symm, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ↔ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ

Tactic:
(memLp_iff hp_pos hp_ne_top).trans integrable_iff.symm

Premises used: MeasureTheory.SimpleFunc.memLp_iff, MeasureTheory.SimpleFunc.integrable_iff, Iff.trans, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ↔ f.FinMeasSupp μ

Tactic:
(memLp_iff hp_pos hp_ne_top).trans finMeasSupp_iff.symm

Premises used: MeasureTheory.SimpleFunc.memLp_iff, Iff.trans, MeasureTheory.SimpleFunc.finMeasSupp_iff, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
⊢ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ ↔ f.FinMeasSupp μ

Tactic:
integrable_iff.trans finMeasSupp_iff.symm

Premises used: MeasureTheory.SimpleFunc.integrable_iff, Iff.trans, MeasureTheory.SimpleFunc.finMeasSupp_iff, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
h : f.FinMeasSupp μ
⊢ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ

Tactic:
integrable_iff_finMeasSupp.2 h

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
μ : Measure α
f : α →ₛ E
g : α →ₛ F
⊢ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ →
    Integrable.{u_5, u_1} (ε := F) (⇑g : (a : α) → F) μ → Integrable (ε := E × F) (⇑(f.pair g) : (a : α) → E × F) μ

Tactic:
simpa only [integrable_iff_finMeasSupp] using FinMeasSupp.pair

Premises used: MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp, MeasureTheory.SimpleFunc.FinMeasSupp.pair
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
f : α →ₛ E
p : ℝ≥0∞
μ : Measure α
inst_2 : IsFiniteMeasure μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
let ⟨C, hfC⟩ := f.exists_forall_norm_le
  MemLp.of_bound f.aestronglyMeasurable C <| Eventually.of_forall hfC

Premises used: MeasureTheory.SimpleFunc.exists_forall_norm_le, Filter.Eventually.of_forall, MeasureTheory.MemLp, _private.0.MeasureTheory.SimpleFunc.memLp_top.match_1, MeasureTheory.MemLp.of_bound, MeasureTheory.SimpleFunc.aestronglyMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α →ₛ E
⊢ Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ

Tactic:
memLp_one_iff_integrable.mp (f.memLp_of_isFiniteMeasure 1 μ)

Premises used: MeasureTheory.SimpleFunc.memLp_of_isFiniteMeasure, Iff.mp, OfNat.ofNat, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
hf : Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
integrable_iff.mp hf x hx

Premises used: MeasureTheory.SimpleFunc.integrable_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
f.measure_support_lt_top ((memLp_iff hp_ne_zero hp_ne_top).mp hf)

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top, MeasureTheory.SimpleFunc.memLp_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
hf : Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
f.measure_support_lt_top (integrable_iff.mp hf)

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top, MeasureTheory.SimpleFunc.integrable_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp.{u_1, u_4} (ε := E) (⇑(piecewise s hs (const α c) (const α 0)) : (a : α) → E) p μ
⊢ Eq.{u_1 + 1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑(const α c) : (a : α) → E)) Set.univ

Tactic:
have : Function.support (const α c) = Set.univ := Function.support_const hc
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp.{u_1, u_4} (ε := E) (⇑(piecewise s hs (const α c) (const α 0)) : (a : α) → E) p μ
this : Eq.{u_1 + 1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑(const α c) : (a : α) → E)) Set.univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [memLp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support,
    support_indicator, Set.inter_univ, this] using hcs

Premises used: Set.inter_univ, MeasureTheory.SimpleFunc.memLp_iff_finMeasSupp, MeasureTheory.SimpleFunc.support_indicator, MeasureTheory.SimpleFunc.finMeasSupp_iff_support
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f g : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
t : α →ₛ E
ht : AEEqFun.mk (⇑t : (a : α) → E) ⋯ = (↑g : α →ₘ[μ] E)
h : AEEqFun.mk (⇑(s + t) : (a : α) → E) ⋯ = (↑(f + g) : α →ₘ[μ] E)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {f : ↥(Lp E p μ) | ∃ (s : α →ₛ E), AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)} (f + g)

Tactic:
use s + t
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f g : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
t : α →ₛ E
ht : AEEqFun.mk (⇑t : (a : α) → E) ⋯ = (↑g : α →ₘ[μ] E)
⊢ AEEqFun.mk (⇑(s + t) : (a : α) → E) ⋯ = (↑(f + g) : α →ₘ[μ] E)

Tactic:
simp only [← hs, ← ht, AEEqFun.mk_add_mk, AddSubgroup.coe_add,
      SimpleFunc.coe_add]

Premises used: MeasureTheory.SimpleFunc.coe_add, AddSubgroup.coe_add, MeasureTheory.AEEqFun.mk_add_mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
h : AEEqFun.mk (⇑(-s) : (a : α) → E) ⋯ = (↑(-f) : α →ₘ[μ] E)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {f : ↥(Lp E p μ) | ∃ (s : α →ₛ E), AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)} (-f)

Tactic:
use -s
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ AEEqFun.mk (⇑(-s) : (a : α) → E) ⋯ = (↑(-f) : α →ₘ[μ] E)

Tactic:
simp only [← hs, AEEqFun.neg_mk, SimpleFunc.coe_neg, AddSubgroup.coe_neg]

Premises used: AddSubgroup.coe_neg, MeasureTheory.AEEqFun.neg_mk, MeasureTheory.SimpleFunc.coe_neg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
⊢ (↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) = (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) → f = g

Tactic:
Subtype.ext ∘ Subtype.ext

Premises used: Function.comp, Subtype.ext
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
rcases :
  ∀ (f : ↥(Lp E p μ)) (s : α →ₛ E) (hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)),
    Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ)
      (k •
        (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)
              f ⋯) :
          ↥(Lp E p μ)))
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) (k • (↑f : ↥(Lp E p μ)))

Tactic:
rcases f with ⟨f, ⟨s, hs⟩⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
h :
  AEEqFun.mk (⇑(k • s) : (a : α) → E) ⋯ =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ)
    (k •
      (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f
            ⋯) :
        ↥(Lp E p μ)))

Tactic:
use k • s
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
apply :
  HSMul.hSMul (β := α →ₘ[μ] E) k (AEEqFun.mk (⇑s : (a : α) → E) ⋯) =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)
⊢ AEEqFun.mk (⇑(k • s) : (a : α) → E) ⋯ =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)

Tactic:
apply Eq.trans (AEEqFun.smul_mk k s s.aestronglyMeasurable).symm _

Premises used: MeasureTheory.AEEqFun.smul_mk, MeasureTheory.SimpleFunc.aestronglyMeasurable, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
rw :
  k • (↑f : α →ₘ[μ] E) =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)
⊢ HSMul.hSMul (β := α →ₘ[μ] E) k (AEEqFun.mk (⇑s : (a : α) → E) ⋯) =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)

Tactic:
rw [hs]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ k • (↑f : α →ₘ[μ] E) =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (↑(c • f) : ↥(Lp E p μ)) = c • (↑f : ↥(Lp E p μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
a : (↑((x * y) • f) : ↥(Lp E p μ)) = (↑(x • y • f) : ↥(Lp E p μ))
⊢ (x * y) • f = x • y • f

Tactic:
ext1