awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
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_2} (ε := ε) (fun (x : α) ↦ c) 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_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]

Premises used: MeasureTheory.lintegral_const, ENNReal.mul_rpow_of_nonneg, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
e_a : (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
⊢ (‖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:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
e_a : ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ

Tactic:
rw [← ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
rw : HPow.hPow (β := ℝ) ‖c‖ₑ 1 = ‖c‖ₑ
rw₁ rw₂ : ‖c‖ₑ = ‖c‖ₑ
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
rw [hq_cancel, ENNReal.rpow_one]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
e_a : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
suffices hq_cancel : q * (1 / q) = 1 by rw [hq_cancel, ENNReal.rpow_one]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
e_a : q * q⁻¹ = 1
e_a₁ e_a₂ : Eq (α := ℝ) 1 1
⊢ q * (1 / q) = 1

Tactic:
rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]

Premises used: mul_inv_cancel₀, Ne.symm, one_div, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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)
rw₁ : ‖c‖ₑ ^ q ≠ ∞
⊢ eLpNorm'.{u_1, u_5} (ε := F) (fun (x : α) ↦ c) 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)]

Premises used: MeasureTheory.lintegral_const, ENNReal.mul_rpow_of_ne_top, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 : (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
⊢ (‖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:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 : ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ

Tactic:
rw [← ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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‖ₑ
rw₁ rw₂ : ‖c‖ₑ = ‖c‖ₑ
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
rw [hp_cancel, ENNReal.rpow_one]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
suffices hp_cancel : q * (1 / q) = 1 by rw [hp_cancel, ENNReal.rpow_one]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
e_a₁ e_a₂ : Eq (α := ℝ) 1 1
⊢ q * (1 / q) = 1

Tactic:
rw [one_div, mul_inv_cancel₀ hq_ne_zero]

Premises used: mul_inv_cancel₀, one_div
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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‖ₑ ≠ 0

Tactic:
simp [hc_ne_zero]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
finiteness finiteness₁ finiteness₂ finiteness₃ : ‖c‖ₑ ≠ 0 → ‖c‖ₑ ^ q ≠ ∞
⊢ ‖c‖ₑ ^ q ≠ ∞

Tactic:
finiteness [show ‖c‖ₑ ≠ 0 by simp [hc_ne_zero]]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ε
hμ : μ ≠ 0
rw : essSup (fun (x : α) ↦ ‖c‖ₑ) μ = ‖c‖ₑ
rw₁ rw₂ : ‖c‖ₑ = ‖c‖ₑ
⊢ eLpNormEssSup.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) μ = ‖c‖ₑ

Tactic:
rw [eLpNormEssSup_eq_essSup_enorm, essSup_const _ hμ]

Premises used: essSup_const, MeasureTheory.eLpNormEssSup_eq_essSup_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
inst_1 : IsProbabilityMeasure μ
⊢ eLpNorm'.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) q μ = ‖c‖ₑ

Tactic:
simp [eLpNorm'_const c hq_pos, measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.eLpNorm'_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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)
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)
⊢ 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 = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
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:
simp [h_top, eLpNormEssSup_const c hμ]

Premises used: MeasureTheory.eLpNormEssSup_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
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:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', ENNReal.toReal_pos, MeasureTheory.eLpNorm'_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
c : ε
h0 : p ≠ 0
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:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', ENNReal.toReal_pos, MeasureTheory.eLpNorm'_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 ≠ ∞
⊢ 0 < p.toReal

Tactic:
have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
neg :
  ∀ (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∞)

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)

Tactic:
simp only [hμ, Measure.coe_zero, Pi.zero_apply, or_true, ENNReal.zero_lt_top,
      eLpNorm_measure_zero]

Premises used: ENNReal.zero_lt_top, Pi.zero_apply, or_true, MeasureTheory.eLpNorm_measure_zero, MeasureTheory.Measure.coe_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
pos :
  ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔
    ‖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∞)

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
⊢ ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hc, ENNReal.zero_rpow_of_pos hp]

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 :
  ‖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∞)
⊢ eLpNorm.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ < ∞ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [eLpNorm_const' c hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.eLpNorm_const'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
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∞)
⊢ ‖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) ∞

Premises used: Set.univ, eq_or_ne, Top.top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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μ_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:
simp [hc, hμ_top, hp]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
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∞)
⊢ ‖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 [ENNReal.mul_lt_top_iff]

Premises used: ENNReal.mul_lt_top_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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∞)
simpa : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ < ∞
⊢ ‖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:
simpa [hμ, hc, hμ_ne_top, hμ_ne_top.lt_top, hc'.lt_top] using by finiteness

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 ≠ ∞
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∞)
⊢ eLpNorm.{u_1, u_5} (ε := F) (fun (x : α) ↦ c) p μ < ∞ ↔
    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]

Premises used: MeasureTheory.eLpNorm_const_lt_top_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 ≠ ∞
⊢ ‖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:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 μ

Tactic:
⟨aestronglyMeasurable_const, ?_⟩

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.MemLp, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst_2 : IsFiniteMeasure μ
refine : eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
⊢ MemLp.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ

Tactic:
refine ⟨aestronglyMeasurable_const, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 μ < ∞
neg : ∀ (h0 : ¬p = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 μ < ∞

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 μ < ∞
neg : ∀ (hμ : ¬μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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 μ < ∞

Tactic:
simp [hμ]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
neg : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) p μ < ∞

Tactic:
rw [eLpNorm_const c h0 hμ]

Premises used: MeasureTheory.eLpNorm_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
c : E
inst_1 : IsFiniteMeasure μ
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p μ

Tactic:
memLp_const_enorm enorm_ne_top

Premises used: MeasureTheory.memLp_const_enorm, enorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
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) ∞ μ < ∞
neg : ∀ (h : ¬μ = 0), eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞

Tactic:
by_cases h : μ = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
h : μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞

Tactic:
simp [eLpNorm_const _, h, hc.lt_top]

Premises used: Ne.lt_top, MeasureTheory.eLpNorm_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
h : ¬μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε') (fun (x : α) ↦ c) ∞ μ < ∞

Tactic:
simp [eLpNorm_const _, h, hc.lt_top]

Premises used: Ne.lt_top, MeasureTheory.eLpNorm_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
c : E
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) ∞ μ

Tactic:
memLp_top_const_enorm enorm_ne_top

Premises used: MeasureTheory.memLp_top_const_enorm, enorm_ne_top