mathlib3

c3967eb5 - Golf `iso.symm_apply_reachable` proof