mathlib

ff959b99 - fix(tactic/induction): fix generalisation with complex major premise

fix(tactic/induction): fix generalisation with complex major premise The induction' and cases' tactics would previously not generalise the goal correctly when called with a complex term (i.e. not just a local constant) as major premise. E.g. the call `cases' (n + 1)` would fail to replace `n + 1` in the hypothesis `n + 1 = m`, leading to very weird goals.