awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ eLpNorm'.{u_1, u_5} (ε := F) (fun (x : α) ↦ c) q μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have rw : (‖c‖ₑ ^ q) ^ (1 / q) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) =
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, lintegral_const,
    ENNReal.mul_rpow_of_ne_top _ (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
rw :
  (‖c‖ₑ ^ q) ^ (1 / q) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
⊢ eLpNorm'.{u_1, u_5} (ε := F) (fun (x : α) ↦ c) q μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have rw₁ : ‖c‖ₑ ^ q ≠ ∞
Tactic: rw [eLpNorm'_eq_lintegral_enorm, lintegral_const,
    ENNReal.mul_rpow_of_ne_top _ (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have e_a : (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
have e_a : ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
Tactic: rw [← ENNReal.rpow_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
hp_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have rw : HPow.hPow (β := ℝ) ‖c‖ₑ 1 = ‖c‖ₑ
Tactic: rw [hp_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
hp_cancel : q * (1 / q) = 1
rw : HPow.hPow (β := ℝ) ‖c‖ₑ 1 = ‖c‖ₑ
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have rw₁ : ‖c‖ₑ = ‖c‖ₑ
Tactic: rw [hp_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have e_a : q * (1 / q) = 1
Tactic: suffices hp_cancel : q * (1 / q) = 1 by rw [hp_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ q * (1 / q) = 1
have e_a : q * q⁻¹ = 1
Tactic: rw [one_div, mul_inv_cancel₀ hq_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
e_a : q * q⁻¹ = 1
⊢ q * (1 / q) = 1
have e_a₁ : Eq (α := ℝ) 1 1
Tactic: rw [one_div, mul_inv_cancel₀ hq_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞
have finiteness : ‖c‖ₑ ≠ 0 → ‖c‖ₑ ^ q ≠ ∞
Tactic: finiteness [show ‖c‖ₑ ≠ 0 by simp [hc_ne_zero]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ε
hμ : μ ≠ 0
⊢ eLpNormEssSup.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) μ = ‖c‖ₑ
have rw : essSup (fun (x : α) ↦ ‖c‖ₑ) μ = ‖c‖ₑ
Tactic: rw [eLpNormEssSup_eq_essSup_enorm, essSup_const _ hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ε
hμ : μ ≠ 0
rw : essSup (fun (x : α) ↦ ‖c‖ₑ) μ = ‖c‖ₑ
⊢ eLpNormEssSup.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) μ = ‖c‖ₑ
have rw₁ : ‖c‖ₑ = ‖c‖ₑ
Tactic: rw [eLpNormEssSup_eq_essSup_enorm, essSup_const _ hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)
have pos : ∀ (h_top : p = ∞),
  eLpNorm.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
pos :
  ∀ (h_top : p = ∞),
    eLpNorm.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) p μ =
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)
have neg : ∀ (h_top : ¬p = ∞),
  eLpNorm.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have hp : 0 < p.toReal
Tactic: have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (hμ : μ = 0),
  eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
pos :
  ∀ (hμ : μ = 0),
    eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
      ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (hμ : ¬μ = 0),
  eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (hc : ‖c‖ₑ = 0),
  eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hc : ‖c‖ₑ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
pos :
  ∀ (hc : ‖c‖ₑ = 0),
    eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
      ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (hc : ¬‖c‖ₑ = 0),
  eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hc : ‖c‖ₑ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ‖c‖ₑ = 0
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔ ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
  ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [eLpNorm_const' c hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (hμ_top : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain hμ_top | hμ_ne_top := eq_or_ne (μ .univ) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
neg :
  ∀ (hμ_top : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
      ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg₁ : ∀ (hμ_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain hμ_top | hμ_ne_top := eq_or_ne (μ .univ) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ‖c‖ₑ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ∨
    ‖c‖ₑ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) = 0 ↔
  ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [ENNReal.mul_lt_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖c‖ₑ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞ ∨
      ‖c‖ₑ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) = 0 ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have simpa : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ < ∞
Tactic: simpa [hμ, hc, hμ_ne_top, hμ_ne_top.lt_top, hc'.lt_top] using by finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ eLpNorm.{u_1, u_5} (ε := F) (fun (x : α) ↦ c) p μ < ∞ ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [eLpNorm_const_lt_top_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
⊢ MemLp.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ
have refine : eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
Tactic: refine ⟨aestronglyMeasurable_const, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
have pos : ∀ (h0 : p = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
pos : ∀ (h0 : p = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
have neg : ∀ (h0 : ¬p = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
h0 : ¬p = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
have pos : ∀ (hμ : μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
h0 : ¬p = 0
pos : ∀ (hμ : μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
have neg : ∀ (hμ : ¬μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
have neg : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
Tactic: rw [eLpNorm_const c h0 hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
have pos : ∀ (h : μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
Tactic: by_cases h : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
pos : ∀ (h : μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
have neg : ∀ (h : ¬μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
Tactic: by_cases h : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p μ ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [memLp_const_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)
have h₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
Tactic: gcongr ?_ ^ (1 / q)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
have h₁ : ∀ (x : α) (hx : ‖f x‖ₑ ≤ ‖g x‖ₑ), ‖f x‖ₑ ^ q ≤ ‖g x‖ₑ ^ q
Tactic: refine lintegral_mono_ae (h.mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ eLpNorm' f q μ = eLpNorm' g q μ
have this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q
Tactic: have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
⊢ eLpNorm' f q μ = eLpNorm' g q μ
have this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q
Tactic: have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [enorm, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ∞ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ
have pos : p = 0 → LE.le (α := ℝ≥0∞) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
pos : p = 0 → LE.le (α := ℝ≥0∞) 0 0
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ∞ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ
have pos₁ : ¬p = 0 → p = ∞ → eLpNormEssSup f μ ≤ eLpNormEssSup g μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
pos : p = 0 → LE.le (α := ℝ≥0∞) 0 0
pos₁ : ¬p = 0 → p = ∞ → eLpNormEssSup f μ ≤ eLpNormEssSup g μ
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ∞ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ
have neg : ¬p = 0 → ¬p = ∞ → eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inl : ∀ (hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C),
  @eLpNorm _ _ _ m0 f p 0 ≤
    C • HPow.hPow (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, hfC