  We describe a recently developed algebraic framework for proving first-order
statements about linear operators by computations with noncommutative
polynomials. Furthermore, we present our new SageMath package operator_gb,
which offers functionality for automatising such computations. We aim to
provide a practical understanding of our approach and the software through
examples, while also explaining the completeness of the method in the sense
that it allows to find algebraic proofs for every true first-order operator
statement. We illustrate the capability of the framework in combination with
our software by a case study on statements about the Moore-Penrose inverse,
including classical facts and recent results, presented in an online notebook.
