Commit 2023-03-27 03:38 50c0cdf6
View on Github →feat: strengthen apply_fun capabilities (#2942)
Use Lean.MVarId.congrN! rather than Lean.MVarId.congrN when proving congruence. This lets apply_fun Fintype.card at h work (note that there are Fintype instances involved, so it needs to apply Subsingleton.elim).