awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ 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)
have 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)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ 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)
have 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)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hp_pos_real : 0 < p.toReal
Tactic: have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hf_eLpNorm : eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞
Tactic: have hf_eLpNorm := MemLp.eLpNorm_lt_top hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 μ < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hf_eLpNorm₁ : ∀ 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
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥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∞) <
      ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (hyf : y ∈ f.range),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hyf : y ∈ f.range
-- 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 : ℝ≥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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (hyf : y ∉ f.range),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hyf : y ∈ f.range
-- 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 : ℝ≥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∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [h_empty, measure_empty]
-- 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 : ℝ≥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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : Eq.{u_1 + 1} (α := Set α) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) ∅
Tactic: suffices h_empty : f ⁻¹' {y} = ∅ by
      rw [h_empty, measure_empty]; exact ENNReal.coe_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hf_eLpNorm₁ : HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
    ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
  ∞
Tactic: specialize hf_eLpNorm y hyf
Cleared hypotheses: hf_eLpNorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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∞) <
    ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: rw [ENNReal.mul_lt_top_iff] at hf_eLpNorm
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥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∞)
have pos : y = 0
Tactic: refine absurd ?_ hy_ne
-- 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 : ℝ≥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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 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]
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
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]
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
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]
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
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]
Cleared hypotheses: hf_eLpNorm
-- 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 : ℝ≥0∞
f : α →ₛ E
hf :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
have pos : ∀ (hp0 : p = 0), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: by_cases hp0 : p = 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
μ : 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 μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
have neg : ∀ (hp0 : ¬p = 0), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: by_cases hp0 : p = 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
μ : 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
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
have pos : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ
Tactic: rw [hp0, memLp_zero_iff_aestronglyMeasurable]
-- 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 : ℝ≥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
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
have pos : ∀ (hp_top : p = ∞), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: by_cases hp_top : p = ∞
-- 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 : ℝ≥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 μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
have neg : ∀ (hp_top : ¬p = ∞), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: by_cases hp_top : p = ∞
-- 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 : ℝ≥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 μ
have pos : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) ∞ μ
Tactic: rw [hp_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
μ : 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 μ
have neg : eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞
Tactic: refine ⟨f.aestronglyMeasurable, ?_⟩
-- 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 : ℝ≥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 = ∞
⊢ eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ < ∞
have 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) <
  ∞
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]
-- 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 : ℝ≥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 = ∞
⊢ 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) <
    ∞
have neg : ∀ y ∈ f.range,
  HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞
Tactic: refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne
-- 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 : ℝ≥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
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞
have pos : ∀ (hy0 : 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
-- 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 : ℝ≥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∞) <
      ∞
⊢ HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {y}) : ℝ≥0∞) <
    ∞
have neg : ∀ (hy0 : ¬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
-- 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 : ℝ≥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∞) <
    ∞
have neg : ‖y‖ₑ ^ p.toReal < ∞
Tactic: refine ENNReal.mul_lt_top ?_ (hf y hy0)