[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ IsSymm (Matrix.fromBlocks A B C D)
[PROOFSTEP]
have hCB : Cᵀ = B := by
  rw [← hBC]
  simp
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Cᵀ = B
[PROOFSTEP]
rw [← hBC]
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Bᵀᵀ = B
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ IsSymm (Matrix.fromBlocks A B C D)
[PROOFSTEP]
unfold Matrix.IsSymm
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [fromBlocks_transpose]
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [hA, hCB, hBC, hD]
