n : Type ?u.121810
p : Type ?u.121813
q : Type ?u.121816
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
inst✝ : Invertible 2
⊢ fromBlocks (1 ⬝ (⅟2 • 1ᵀ) + (-1) ⬝ (⅟2 • (-1)ᵀ)) (1 ⬝ (⅟2 • 1ᵀ) + (-1) ⬝ (⅟2 • 1ᵀ)) (1 ⬝ (⅟2 • 1ᵀ) + 1 ⬝ (⅟2 • (-1)ᵀ))
      (1 ⬝ (⅟2 • 1ᵀ) + 1 ⬝ (⅟2 • 1ᵀ)) =
    1
n : Type ?u.121810
p : Type ?u.121813
q : Type ?u.121816
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
inst✝ : Invertible 2
⊢ PD l R * ⅟2 • (PD l R)ᵀ = 1
rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul, Matrix.mul_eq_mul,
  Matrix.fromBlocks_multiply]
no goals
n : Type ?u.121810
p : Type ?u.121813
q : Type ?u.121816
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
inst✝ : Invertible 2
⊢ fromBlocks (1 ⬝ (⅟2 • 1ᵀ) + (-1) ⬝ (⅟2 • (-1)ᵀ)) (1 ⬝ (⅟2 • 1ᵀ) + (-1) ⬝ (⅟2 • 1ᵀ)) (1 ⬝ (⅟2 • 1ᵀ) + 1 ⬝ (⅟2 • (-1)ᵀ))
      (1 ⬝ (⅟2 • 1ᵀ) + 1 ⬝ (⅟2 • 1ᵀ)) =
    1
simp