no goals
ι : Type ?u.1855701
ι' : Type ?u.1855704
𝕜 : Type u_3
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1855713
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1855733
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1855751
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1855771
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
m : Type u_2
n : Type u_1
inst✝ : Fintype n
A B : Matrix m n 𝕜
i j : m
⊢ inner (↑(PiLp.equiv 2 fun i => 𝕜).symm (A i)) (↑(PiLp.equiv 2 fun i => 𝕜).symm (B j)) = (B ⬝ Aᴴ) j i
simp_rw [EuclideanSpace.inner_piLp_equiv_symm, Matrix.mul_apply', Matrix.dotProduct_comm,
  Matrix.conjTranspose_apply, Pi.star_def]