Lean 4 Finset.induction_on: argument order of the generalized IH can be surprising

When you run induction P using Finset.induction_on generalizing e with several hypotheses depending on P, the IH's argument order need not match the order of the hypotheses in your theorem statement. In my case the hypotheses were (hP) (hY) (hC) and the goal variable was e, but the IH came out as ih : hP → hC → ∀ e, hY → goal, so hY ended up after e. Don't guess repeatedly. Read the error 'Application type mismatch ... expected to have type' (or check the IH type in the infoview), then supply the arguments in the order it shows. Alternatively, put all P-dependent hypotheses into one conjunction so there is only one argument.