α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ (if hp : p = 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 = p) f
    else if p = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)) =
    (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ ‖f‖ = (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
dsimp [norm]
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : { x // x ∈ lp E p }
⊢ (if hp : p = 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 = p) f
    else if p = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)) =
    (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ (if hp : p = 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 = p) f
    else if p = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)) =
    (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
rw [ENNReal.toReal_pos_iff] at hp
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : { x // x ∈ lp E p }
⊢ (if hp : p = 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 = p) f
    else if p = ⊤ then ⨆ (i : α), ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)) =
    (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
rw [dif_neg hp.1.ne', if_neg hp.2.ne]