no goals
p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.533812
ι : Type u_1
α : ι → Type ?u.533820
β : ι → Type ?u.533825
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.534021
inst✝³ : Fintype ι'
E : Type ?u.534027
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
⊢ ↑(basisFun p 𝕜 ι) i = ↑(PiLp.equiv p fun i => 𝕜).symm (Pi.single i 1)
simp_rw [basisFun, Basis.coe_ofEquivFun, PiLp.linearEquiv_symm_apply, Pi.single]