α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
⊢ (if hp : ⊤ = 0 then
      Eq.rec (motive := fun x x_1 => { x_2 // x_2 ∈ lp E x } → ℝ)
        (fun f => ↑(Finset.card (Set.Finite.toFinset (_ : Set.Finite {i | ↑f i ≠ 0})))) (_ : 0 = ⊤) f
    else if ⊤ = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ 0) ^ (1 / 0)) =
    ⨆ (i : α), ‖↑f i‖
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
⊢ ‖f‖ = ⨆ (i : α), ‖↑f i‖
dsimp [norm]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
⊢ (if hp : ⊤ = 0 then
      Eq.rec (motive := fun x x_1 => { x_2 // x_2 ∈ lp E x } → ℝ)
        (fun f => ↑(Finset.card (Set.Finite.toFinset (_ : Set.Finite {i | ↑f i ≠ 0})))) (_ : 0 = ⊤) f
    else if ⊤ = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ 0) ^ (1 / 0)) =
    ⨆ (i : α), ‖↑f i‖
rw [dif_neg ENNReal.top_ne_zero, if_pos rfl]