mathlib3

37bbbeb4 - Refactor simplify_ih and related functions