Minimalistic online IDE (no installation needed; just copypaste the code and walk through the proof)
Natural Number Game (fun interactive tutorial by Kevin Buzzard et al.)
Overview of basic tactics (things you use in proofs, not definitions)
Code from my minicourse (took place at ISTA in 2023-09)