mathlib documentation

core / init.meta.congr_tactic