Using Lean like a CAS

Stream: new members

[Mr Proof]

I found some ways to use Lean like a Computer Algebra System (CAS) to do simple calculations. This doesn't produce proofs but by looking in the output window you can see the calculations:

Expand
Say I want to find the expansion of (x+y)^3

I can write:

import Mathlib
example: (expr:Rat) = (x+y)^4 :=by ring_nf

Multiply matrices
Multiplying matrices of variables. (Have to specify the type of at least one).

import Mathlib
example:  expr = !![(a:Rat),b;c,d] * !![e,f;g,h]  :=by simp

Expand numerical expesssions
Isn't always easiest to get it to the simplest form:

example: (expr:Real) = (√3 + 1)^2 := by ring_nf;rw[Real.sq_sqrt];ring_nf

I don't think it can do factorisation. Do you know any other simple "hacks" to do CAS-like calculations?