no goals
p : ℝ≥0∞
𝕜 : Type ?u.509175
𝕜' : Type ?u.509178
ι : Type u_2
α : ι → Type ?u.509186
β✝ : ι → Type ?u.509191
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.509387
inst✝⁴ : Fintype ι'
E : Type ?u.509393
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊) = ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * ‖b‖
simp