awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
fmeas : Measurable f
hf : Integrable f μ
⊢ HasFiniteIntegral.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) μ

Tactic:
simpa using hf.2

Premises used: And.right
-- 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 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : Integrable f μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : Integrable f μ
n : ℕ
⊢ Integrable.{u_4, u_2} (ε := E) (⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) : (a : β) → E) μ

Tactic:
integrable_approxOn fmeas hf _ (integrable_zero _ _ _) n

Premises used: MeasureTheory.integrable_zero, MeasureTheory.SimpleFunc.integrable_approxOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
f : α →ₛ F
⊢ ∃ (C : ℝ), ∀ (x : α), norm.{u_5} (E := F) ((f : (a : α) → F) x : F) ≤ C

Tactic:
exists_forall_le (f.map fun x => ‖x‖)

Premises used: MeasureTheory.SimpleFunc.exists_forall_le, Norm.norm, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
f : α →ₛ E
μ : Measure α
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) 0 μ

Tactic:
memLp_zero_iff_aestronglyMeasurable.mpr f.aestronglyMeasurable

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.memLp_zero_iff_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
f : α →ₛ E
μ : Measure α
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) ∞ μ

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

Premises used: MeasureTheory.memLp_top_of_bound, MeasureTheory.SimpleFunc.exists_forall_norm_le, Filter.Eventually.of_forall, MeasureTheory.MemLp, _private.0.MeasureTheory.SimpleFunc.memLp_top.match_1, MeasureTheory.SimpleFunc.aestronglyMeasurable, Top.top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
    ((fun (x : F) ↦ ‖x‖ₑ ^ p) ∘ (⇑f : (a : α) → F))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ Eq (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
    (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞)

Tactic:
have h_map : (‖f ·‖ₑ ^ p) = f.map (‖·‖ₑ ^ p) := by simp; rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map :
  Eq (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
    (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞)
rw :
  (∫⁻ (a : α), enorm.{u_5} (E := F) ((f : (a : α) → F) a : F) ^ p ∂μ) ^ (1 / p) =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
rw₁ :
  MeasureTheory.lintegral μ (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞) ^ (1 / p) =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
rw₂ :
  lintegral (map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) μ ^ (1 / p) =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
rw₃ rw₄ :
  HPow.hPow (α := ℝ≥0∞)
      (∑ x ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖x‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : ℝ≥0∞))
      (1 / p) =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
⊢ eLpNorm'.{u_1, u_5} (ε := F) (⇑f : (a : α) → F) p μ =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]

Premises used: MeasureTheory.SimpleFunc.map_lintegral, MeasureTheory.eLpNorm'_eq_lintegral_enorm, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
⊢ 0 < p.toReal

Tactic:
have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
⊢ eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞

Tactic:
have hf_eLpNorm := MemLp.eLpNorm_lt_top hf
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞))
      p.toReal⁻¹ <
    ∞
⊢ 0 < p.toReal⁻¹

Tactic:
simp [hp_pos_real]
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∑ y ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    HPow.hPow (α := ℝ≥0∞) ∞ p.toReal⁻¹⁻¹
⊢ 0 < p.toReal⁻¹⁻¹

Tactic:
simp [hp_pos_real]
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞
⊢ ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp_pos hp_ne_top, f.eLpNorm'_eq, one_div,
    ← @ENNReal.lt_rpow_inv_iff _ _ p.toReal⁻¹ (by simp [hp_pos_real]),
    @ENNReal.top_rpow_of_pos p.toReal⁻¹⁻¹ (by simp [hp_pos_real]),
    ENNReal.sum_lt_top] at hf_eLpNorm

Premises used: ENNReal.lt_rpow_inv_iff, MeasureTheory.eLpNorm_eq_eLpNorm', ENNReal.sum_lt_top, ENNReal.top_rpow_of_pos, MeasureTheory.SimpleFunc.eLpNorm'_eq, one_div
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
pos :
  ∀ (hyf : y ∈ f.range),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
neg :
  ∀ (hyf : y ∉ f.range),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_cases hyf : y ∈ f.range

Premises used: MeasureTheory.SimpleFunc.range
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
h_empty : Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅
rw : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [h_empty, measure_empty]

Premises used: MeasureTheory.measure_empty
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
h_empty : Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
h_empty : Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
neg : Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices h_empty : f ⁻¹' {y} = ∅ by
      rw [h_empty, measure_empty]; exact ENNReal.coe_lt_top
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
⊢ Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅

Tactic:
(preimage_eq_empty_iff _ _).mpr hyf

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.preimage_eq_empty_iff
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∉ f.range
⊢ Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅

Tactic:
exact (preimage_eq_empty_iff _ _).mpr hyf

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.preimage_eq_empty_iff
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (‖a‖ₑ ^ p.toReal)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) <
      ∞
hyf : y ∈ f.range
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞

Tactic:
specialize hf_eLpNorm y hyf
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm :
  HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞
⊢ ‖y‖ₑ ^ p.toReal < ∞ ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    ‖y‖ₑ ^ p.toReal = 0 ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [ENNReal.mul_lt_top_iff] at hf_eLpNorm

Premises used: ENNReal.mul_lt_top_iff
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm :
  ‖y‖ₑ ^ p.toReal < ∞ ∧
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hf_eLpNorm.2

Premises used: And.right
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm :
  ‖y‖ₑ ^ p.toReal < ∞ ∧
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hf_eLpNorm.2

Premises used: And.right
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
absurd ?_ hy_ne

Premises used: absurd
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 0
pos : y = 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine absurd ?_ hy_ne

Premises used: absurd
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 0
⊢ y = 0

Tactic:
simpa [hp_pos_real] using hf_eLpNorm
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hf_eLpNorm]
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm :
  ‖y‖ₑ ^ p.toReal = 0 ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 0),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
pos₁ :
  ∀
    (hf_eLpNorm :
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
cases hf_eLpNorm with
    | inl hf_eLpNorm =>
      refine absurd ?_ hy_ne
      simpa [hp_pos_real] using hf_eLpNorm
    | inr hf_eLpNorm => simp [hf_eLpNorm]

Premises used: absurd
-- 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 ≠ ∞
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm :
  ‖y‖ₑ ^ p.toReal < ∞ ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    ‖y‖ₑ ^ p.toReal = 0 ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀
    (hf_eLpNorm :
      ‖y‖ₑ ^ p.toReal < ∞ ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
pos₁ :
  ∀
    (hf_eLpNorm :
      ‖y‖ₑ ^ p.toReal = 0 ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (0 : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
cases hf_eLpNorm with
  | inl hf_eLpNorm => exact hf_eLpNorm.2
  | inr hf_eLpNorm =>
    cases hf_eLpNorm with
    | inl hf_eLpNorm =>
      refine absurd ?_ hy_ne
      simpa [hp_pos_real] using hf_eLpNorm
    | inr hf_eLpNorm => simp [hf_eLpNorm]

Premises used: absurd
-- 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∞)
pos : ∀ (hp0 : p = 0), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
neg : ∀ (hp0 : ¬p = 0), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
by_cases hp0 : p = 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
pos : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
rw [hp0, memLp_zero_iff_aestronglyMeasurable]

Premises used: MeasureTheory.memLp_zero_iff_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
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ

Tactic:
f.aestronglyMeasurable

Premises used: 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
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ

Tactic:
exact f.aestronglyMeasurable

Premises used: 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
pos : ∀ (hp_top : p = ∞), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
neg : ∀ (hp_top : ¬p = ∞), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
by_cases hp_top : p = ∞