1. repeat can use before rw, to repeat rw until can't. repeat rw [something]
2. basically it can prove something use rfl(same between "=") exact( same as hd in the induction or the required precondition.)