Formalising mathematics in Lean and Mathlib

With f : α → β and g : β → γ, which Lean statement says that a composite of injective functions is injective?

To prove that $g \circ f$ is injective, we assume $g(f(x)) = g(f(y))$ and must show $x = y$. Which fact do we use first?

Which function $f : \N \to \N$ gives sets $S, T$ with $f(S \cap T) \ne f(S) \cap f(T)$?

Which of these statements about natural numbers are true? (Choose all that apply.)

In Lean, with natural numbers, what is the value of (5 : ℕ) - 8 + 8?

In Mathlib, (7 : ℝ) / 0 = 0 is a theorem (div_zero). What follows?

#print axioms limit_unique reports [propext, Classical.choice, Quot.sound]. What does this tell you?

In the proof that a group in which every $x$ satisfies $x^2 = 1$ is commutative, we write $ab = (ab)^{-1} = b^{-1}a^{-1} = ba$. Which group law justifies the middle equality?

Write find_counterexample(a, b) that searches all functions $f$ from $\{0, \dots, a-1\}$ to $\{0, \dots, b-1\}$ (as tuples of values) and all pairs of subsets $S, T$ of the domain, and returns the first (f, S, T) with $f(S \cap T) \ne f(S) \cap f(T)$ (with S, T as Python sets), or None if there is none. Use itertools.