n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ ⬝ JD l R ⬝ PD l R = 2 • S l R
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
⊢ (PD l R)ᵀ ⬝ JD l R ⬝ PD l R = 2 • S l R
have h : (PD l R)ᵀ ⬝ JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
  simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 ⬝ 1 + 1 ⬝ 1) (1 ⬝ (-1) + 1 ⬝ 1) (1 ⬝ 1 + (-1) ⬝ 1) (1 ⬝ (-1) + (-1) ⬝ 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ ⬝ JD l R ⬝ PD l R = 2 • S l R
rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 ⬝ 1 + 1 ⬝ 1) (1 ⬝ (-1) + 1 ⬝ 1) (1 ⬝ 1 + (-1) ⬝ 1) (1 ⬝ (-1) + (-1) ⬝ 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 ⬝ 1 + 1 ⬝ 1) (1 ⬝ (-1) + 1 ⬝ 1) (1 ⬝ 1 + (-1) ⬝ 1) (1 ⬝ (-1) + (-1) ⬝ 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
congr
no goals
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
h : (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 ⬝ 1 + 1 ⬝ 1) (1 ⬝ (-1) + 1 ⬝ 1) (1 ⬝ 1 + (-1) ⬝ 1) (1 ⬝ (-1) + (-1) ⬝ 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
simp [two_smul]
no goals
n : Type ?u.110673
p : Type ?u.110676
q : Type ?u.110679
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
⊢ (PD l R)ᵀ ⬝ JD l R = fromBlocks 1 1 1 (-1)
simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]