Transformation geometry and the Erlangen programme

What kind of isometry is $f(z) = -z + 4$?

Which of these isometries of the plane move every point? (Choose all that apply.)

Two mirror lines cross at the point $P$ at an angle of $40^\circ$. What is the composite of the two reflections?

The points $0, 1, 3, -3$ have cross-ratio $(0, 1;\, 3, -3) = \dfrac{(3 - 0)(-3 - 1)}{(3 - 1)(-3 - 0)} = 2$. The projective map $m(x) = \dfrac{2x + 1}{x + 1}$ sends them to $1, \tfrac32, \tfrac74, \tfrac52$. What is the cross-ratio $(1, \tfrac32;\, \tfrac74, \tfrac52)$?

Four equally spaced fence posts stand along a straight road. In a photograph, measured along the image of the road, the first three appear at $0$, $10$ and $15$ mm. At how many millimetres does the fourth appear? (Use the cross-ratio: equally spaced points $0, 1, 2, 3$ have $(0, 1; 2, 3) = \tfrac43$.)

Which property is preserved by every affine map $x \mapsto Ax + b$ of the plane?

Claim: an isometry of the plane is determined by the images of two distinct points $p$ and $q$. The claim is false. Which counterexample shows it?

Which Lean statement correctly formalises the glide reflection $z \mapsto \bar z + t$ (with $t$ real and non-zero) has no fixed point?

An isometry is stored as (a, b, opposite) meaning $z \mapsto az + b$ (if opposite is False) or $z \mapsto a\bar z + b$ (if True), with $|a| = 1$. Write classify(a, b, opposite) returning 'identity', 'translation', 'rotation', 'reflection' or 'glide', using the criteria from the proof. The tests use Gaussian integers, so exact comparisons with == are safe.