Pick a diagram. Change it. Reach the goal.

Every change you make is a step. If someone took the same step before, you follow them; if not, you open a new path. When the goal appears, press QED.

Choose a diagram

+ New diagram

Theorem. Snake diagram 2 goals · R-Mod commutes rows exact snake

and 1 more goal

Definition. Short exact sequence 1 goal · R-Mod commutes rows exact short exact

Commutative square 1 goal · R-Mod commutes

$A$ is projective 0 goals · R-Mod commutes rows exact

Attach kernel square 1 goal · R-Mod commutes

Axiom. Take an element 1 goal · R-Mod commutes

Hom out of Y R-Mod → Ab: Attach kernel square 0 goals · Ab commutes

Read the tutorials