p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.557496
ι : Type u_1
α : ι → Type ?u.557504
β : ι → Type ?u.557509
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.557705
inst✝² : Fintype ι'
E : Type ?u.557711
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  Basis.toMatrix (Basis.map b (PiLp.linearEquiv p 𝕜 fun x => 𝕜)) ↑(Pi.basisFun 𝕜 ι) ⬝ A =
    ↑of fun i j => ↑(↑(Basis.map b (PiLp.linearEquiv p 𝕜 fun x => 𝕜)).repr (Aᵀ j)) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) ⬝ A = ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.557496
ι : Type u_1
α : ι → Type ?u.557504
β : ι → Type ?u.557509
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.557705
inst✝² : Fintype ι'
E : Type ?u.557711
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) ⬝ A = ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
have := basis_toMatrix_basisFun_mul (b.map (PiLp.linearEquiv _ 𝕜 _)) A
p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.557496
ι : Type u_1
α : ι → Type ?u.557504
β : ι → Type ?u.557509
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.557705
inst✝² : Fintype ι'
E : Type ?u.557711
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  (Basis.toMatrix b fun x => ↑(basisFun p 𝕜 ι) x) ⬝ A =
    ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) ⬝ A = ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.557496
ι : Type u_1
α : ι → Type ?u.557504
β : ι → Type ?u.557509
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.557705
inst✝² : Fintype ι'
E : Type ?u.557711
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  Basis.toMatrix (Basis.map b (PiLp.linearEquiv p 𝕜 fun x => 𝕜)) ↑(Pi.basisFun 𝕜 ι) ⬝ A =
    ↑of fun i j => ↑(↑(Basis.map b (PiLp.linearEquiv p 𝕜 fun x => 𝕜)).repr (Aᵀ j)) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) ⬝ A = ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply,
  PiLp.linearEquiv_symm_apply, Basis.toMatrix_map, Function.comp, Basis.map_apply,
  LinearEquiv.symm_apply_apply] at this
no goals
p : ℝ≥0∞
𝕜 : Type u_2
𝕜' : Type ?u.557496
ι : Type u_1
α : ι → Type ?u.557504
β : ι → Type ?u.557509
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.557705
inst✝² : Fintype ι'
E : Type ?u.557711
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  (Basis.toMatrix b fun x => ↑(basisFun p 𝕜 ι) x) ⬝ A =
    ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) ⬝ A = ↑of fun i j => ↑(↑b.repr (↑(PiLp.equiv p fun i => 𝕜).symm (Aᵀ j))) i
exact this