-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_const_lt_top_iff {p : ℝ≥0∞} {c : F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    eLpNorm (fun _ : α => c) p μ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
rw [eLpNorm_const' c hp_ne_zero hp_ne_top]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

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

Result:
no goals

Proof state:
case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ ≠ ⊤
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
rw [ENNReal.mul_lt_top_iff]

Result:
case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ ≠ ⊤
⊢ ‖c‖ₑ < ⊤ ∧ μ Set.univ ^ (1 / p.toReal) < ⊤ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
by_cases hμ : μ = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
obtain hμ_top | hμ_top := eq_or_ne (μ .univ) ∞

Result:
case neg.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ = ⊤
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ ≠ ⊤
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
by_cases hc : c = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : c = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Proof state:
case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ ≠ ⊤
⊢ ‖c‖ₑ < ⊤ ∧ μ Set.univ ^ (1 / p.toReal) < ⊤ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
simpa [hμ, hc, hμ_top, hμ_top.lt_top] using
  ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.mpr hp.le) hμ_top

Result:
no goals

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : c = 0
⊢ eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
simp only [hc, true_or, eq_self_iff_true, ENNReal.zero_lt_top, eLpNorm_zero']

Result:
no goals

Proof state:
case neg.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬c = 0
hμ_top : μ Set.univ = ⊤
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
simp [hc, hμ_top, hp]

Result:
no goals