p : ℝ≥0∞
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁴ : Fintype ι'
E : Type ?u.503832
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
p : ℝ≥0∞
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
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.503826
inst✝⁴ : Fintype ι'
E : Type ?u.503832
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
clear x y
case inl
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedField 𝕜
inst✝⁸ : NormedField 𝕜'
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁵ : Fintype ι'
E : Type ?u.503832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
β : Type u_1
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty ι
b : β
inst✝ : Fact (1 ≤ ⊤)
⊢ ‖↑(PiLp.equiv ⊤ fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / ⊤) * ‖b‖₊

case inr
p : ℝ≥0∞
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁴ : Fintype ι'
E : Type ?u.503832
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ⊤
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
p : ℝ≥0∞
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁴ : Fintype ι'
E : Type ?u.503832
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
rcases em <| p = ∞ with (rfl | hp)
no goals
case inl
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedField 𝕜
inst✝⁸ : NormedField 𝕜'
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁵ : Fintype ι'
E : Type ?u.503832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
β : Type u_1
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty ι
b : β
inst✝ : Fact (1 ≤ ⊤)
⊢ ‖↑(PiLp.equiv ⊤ fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / ⊤) * ‖b‖₊
simp only [equiv_symm_apply, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, one_mul,
  nnnorm_eq_ciSup, Function.const_apply, ciSup_const]
no goals
case inr
p : ℝ≥0∞
𝕜 : Type ?u.503614
𝕜' : Type ?u.503617
ι : Type u_2
α : ι → Type ?u.503625
β✝ : ι → Type ?u.503630
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.503826
inst✝⁴ : Fintype ι'
E : Type ?u.503832
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_1
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ⊤
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
exact nnnorm_equiv_symm_const hp b