Commit 2024-03-01 13:29 2a70ed26

refactor: induction₂_symm: Be more explicit in the case variables (#11023) and in setToL1_mono_left, instantiate the induction theorem explicitly. In https://github.com/leanprover/lean4/pull/3505 I am fixing a big where induction will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for foralls; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.