no goals
n : Type ?u.156835
p : Type ?u.156838
q : Type ?u.156841
l : Type u_1
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ (PB l R)ᵀ ⬝ JB l R ⬝ PB l R = 2 • fromBlocks 1 0 0 (S l R)
simp [PB, JB, jd_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply,
  Matrix.fromBlocks_smul]