case inl
α : Type u_1
E : Type ?u.915301
F : Type u_2
G : Type ?u.915307
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq0 : 0 ≤ q
⊢ snorm' 0 q μ = 0

case inr
α : Type u_1
E : Type ?u.915301
F : Type u_2
G : Type ?u.915307
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq_neg : q < 0
⊢ snorm' 0 q μ = 0
α : Type u_1
E : Type ?u.915301
F : Type u_2
G : Type ?u.915307
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hq0_ne : q ≠ 0
hμ : μ ≠ 0
⊢ snorm' 0 q μ = 0
cases' le_or_lt 0 q with hq0 hq_neg
no goals
case inl
α : Type u_1
E : Type ?u.915301
F : Type u_2
G : Type ?u.915307
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq0 : 0 ≤ q
⊢ snorm' 0 q μ = 0
exact snorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)
no goals
case inr
α : Type u_1
E : Type ?u.915301
F : Type u_2
G : Type ?u.915307
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq_neg : q < 0
⊢ snorm' 0 q μ = 0
simp [snorm', ENNReal.rpow_eq_zero_iff, hμ, hq_neg]