awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : Ne (α := ℝ≥0∞) 0 ∞
hf : MemLp f 0 μ
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε
have h : MeasurableSet.{u_1} (α := α) ∅ ∧
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (Set.indicator ∅ᶜ f) 0 μ < ε
Tactic: use ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
have hf₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
Tactic: apply exists_setLIntegral_compl_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
hf₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
have hε₁ : ε ^ p.toReal ≠ 0
Tactic: apply exists_setLIntegral_compl_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
have inr : ∀ (s : Set α) (hsm : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal),
  ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
Tactic: obtain ⟨s, hsm, hs, hε⟩ :
        ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, (‖f a‖ₑ) ^ p.toReal ∂μ < ε ^ p.toReal := by
      apply exists_setLIntegral_compl_lt
      · exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne
      · simp [*]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
have inr : eLpNorm (sᶜ.indicator f) p μ < ε
Tactic: refine ⟨s, hsm, hs, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ eLpNorm (sᶜ.indicator f) p μ < ε
have inr : 0 < p.toReal
Tactic: rwa [eLpNorm_indicator_eq_eLpNorm_restrict hsm.compl,
      eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp_top, one_div, ENNReal.rpow_inv_lt_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal = lpNorm f p μ
have rw : (eLpNorm f p μ).toReal = if AEStronglyMeasurable f μ then (eLpNorm f p μ).toReal else 0
Tactic: rw [lpNorm, if_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
rw : (eLpNorm f p μ).toReal = if AEStronglyMeasurable f μ then (eLpNorm f p μ).toReal else 0
⊢ (eLpNorm f p μ).toReal = lpNorm f p μ
have rw₁ : (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal
Tactic: rw [lpNorm, if_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ ENNReal.ofReal (lpNorm f p μ) = eLpNorm f p μ
have rw : ENNReal.ofReal (eLpNorm f p μ).toReal = eLpNorm f p μ
Tactic: rw [← toReal_eLpNorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal hf.eLpNorm_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
rw : ENNReal.ofReal (eLpNorm f p μ).toReal = eLpNorm f p μ
⊢ ENNReal.ofReal (lpNorm f p μ) = eLpNorm f p μ
have rw₁ : eLpNorm f p μ = eLpNorm f p μ
Tactic: rw [← toReal_eLpNorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal hf.eLpNorm_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ lpNorm f p μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
have rw : HPow.hPow (α := ℝ) (∫ (a : α), (‖f a‖ₑ ^ p.toReal).toReal ∂μ) (1 / p.toReal) =
  HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
Tactic: rw [← toReal_eLpNorm hf, eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp, ← ENNReal.toReal_rpow,
    ← integral_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
rw :
  HPow.hPow (α := ℝ) (∫ (a : α), (‖f a‖ₑ ^ p.toReal).toReal ∂μ) (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
⊢ lpNorm f p μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
have hfm : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
Tactic: rw [← toReal_eLpNorm hf, eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp, ← ENNReal.toReal_rpow,
    ← integral_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
rw :
  HPow.hPow (α := ℝ) (∫ (a : α), (‖f a‖ₑ ^ p.toReal).toReal ∂μ) (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
hfm : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
⊢ lpNorm f p μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
have hf₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ^ p.toReal < ∞
Tactic: rw [← toReal_eLpNorm hf, eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp, ← ENNReal.toReal_rpow,
    ← integral_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have hfm : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal ‖f x‖ ^ p.toReal) μ
Tactic: simp_rw [← ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal ‖f x‖ ^ p.toReal) μ
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
⊢ lpNorm f (↑p : ℝ≥0∞) μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ) ∂μ) (↑p : ℝ)⁻¹
have rw : HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ≥0∞).toReal ∂μ) (↑p : ℝ≥0∞).toReal⁻¹ =
  HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ) ∂μ) (↑p : ℝ)⁻¹
Tactic: rw [lpNorm_eq_integral_norm_rpow_toReal (by positivity) (by simp) hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ lpNorm f ∞ μ = essSup (fun (x : α) ↦ ‖f x‖) μ
have simp : ENNReal.toReal (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) = essSup (fun (x : α) ↦ ‖f x‖) μ
Tactic: simp only [← toReal_eLpNorm hf.aestronglyMeasurable, eLpNorm_exponent_top, eLpNormEssSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ ENNReal.toReal (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) = essSup (fun (x : α) ↦ ‖f x‖) μ
have refine : ∀ᶠ (x : ℝ) in map (fun (i : α) ↦ ‖f i‖ₑ.toReal) (ae μ), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (lpNorm f ∞ μ)
Tactic: refine ENNReal.toReal_essSup (by simp) ⟨lpNorm f ∞ μ, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (-f) p μ = lpNorm f p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (-f) p μ = lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (-f) p μ = lpNorm f p μ
⊢ lpNorm (-f) p μ = lpNorm f p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm (-f) p μ = lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm (-f) p μ = lpNorm f p μ
have neg : lpNorm (-f) p μ = 0
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf,
      lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by simpa using h.neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
neg : lpNorm (-f) p μ = 0
⊢ lpNorm (-f) p μ = lpNorm f p μ
have neg₁ : Eq (α := ℝ) 0 0
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf,
      lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by simpa using h.neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f - g) p μ = lpNorm (g - f) p μ
have rw : lpNorm (-(f - g)) p μ = lpNorm (g - f) p μ
Tactic: rw [← lpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ = lpNorm f p μ
have rw : (eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ).toReal = (eLpNorm f p μ).toReal
Tactic: rw [← toReal_eLpNorm hf, ← toReal_eLpNorm (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
have neg : lpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = (↑(nnnorm.{u_3} (E := 𝕜) 0) : ℝ) * lpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
neg : lpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = (↑(nnnorm.{u_3} (E := 𝕜) 0) : ℝ) * lpNorm f p μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
have neg₁ : ∀ (hc : c ≠ 0), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
hc : c ≠ 0
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
have neg : 0 = (↑‖c‖₊ : ℝ) * 0
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
    simpa [hc] using h.const_smul c⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : CharZero 𝕜
n : ℕ
hn : n ≠ 0
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f / (↑n : α → 𝕜)) p μ = lpNorm f p μ / (↑n : ℝ)
have rw : lpNorm (f / (↑n : α → 𝕜) * (↑n : α → 𝕜)) p μ = lpNorm f p μ
Tactic: rw [eq_div_iff (by positivity), ← lpNorm_mul_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
have pos : ∀ (hg : MemLp g p μ), lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
Tactic: by_cases hg : MemLp g p μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
pos : ∀ (hg : MemLp g p μ), lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
have neg : ∀ (hg : ¬MemLp g p μ), lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
Tactic: by_cases hg : MemLp g p μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
have pos : (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal
Tactic: rw [← toReal_eLpNorm (hf.add hg).aestronglyMeasurable,
      ← toReal_eLpNorm hf.aestronglyMeasurable, ← toReal_eLpNorm hg.aestronglyMeasurable,
      ← ENNReal.toReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal
have pos : eLpNorm f p μ + eLpNorm g p μ ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
pos : eLpNorm f p μ + eLpNorm g p μ ≠ ∞
⊢ (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal
have pos₁ : eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
have neg : 0 ≤ lpNorm f p μ + 0
Tactic: rw [lpNorm_of_not_memLp fun hfg ↦ hg <| by simpa using hfg.sub hf, lpNorm_of_not_memLp hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, lpNorm (f i) p μ
have rw : (eLpNorm.{u_1, u_2} (ε := E) (∑ i ∈ s, f i) p μ).toReal ≤ ENNReal.toReal (∑ a ∈ s, eLpNorm (f a) p μ)
Tactic: rw [← Finset.sum_congr rfl fun i hi ↦ toReal_eLpNorm (hf i hi).aestronglyMeasurable,
    ← ENNReal.toReal_sum fun i hi ↦ (hf i hi).2.ne,
    ← toReal_eLpNorm (Finset.aestronglyMeasurable_sum _ fun i hi ↦ (hf i hi).aestronglyMeasurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ (eLpNorm.{u_1, u_2} (ε := E) (∑ i ∈ s, f i) p μ).toReal ≤ ENNReal.toReal (∑ a ∈ s, eLpNorm (f a) p μ)
have h₁ : Ne (α := ℝ≥0∞) (∑ i ∈ s, eLpNorm (f i) p μ) ∞
Tactic: grw [eLpNorm_sum_le (fun i hi ↦ (hf _ hi).aestronglyMeasurable) hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
have inl : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
  lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ ∅, f i) p μ ≤ 𝔼 i ∈ ∅, lpNorm (f i) p μ
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
inl :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
    lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ ∅, f i) p μ ≤ 𝔼 i ∈ ∅, lpNorm (f i) p μ
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
have inr : ∀ (hs : s.Nonempty), lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
have inr : HSMul.hSMul (α := ℚ≥0) (↑s.card : ℚ≥0) (lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ) ≤
  ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i
Tactic: refine (le_inv_smul_iff_of_pos <| by positivity).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ HSMul.hSMul (α := ℚ≥0) (↑s.card : ℚ≥0) (lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ) ≤
    ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i
have inr : lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i
Tactic: rw [Nat.cast_smul_eq_nsmul, ← lpNorm_nsmul, Finset.card_smul_expect]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
⊢ lpNorm f p μ ≤ lpNorm g p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p μ ≤ lpNorm g p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p μ ≤ lpNorm g p μ
⊢ lpNorm f p μ ≤ lpNorm g p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p μ ≤ lpNorm g p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
⊢ lpNorm f p μ ≤ lpNorm g p μ
have pos : (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal
Tactic: rw [← toReal_eLpNorm hf, ← toReal_eLpNorm hg.aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ