Commit 2026-10-24 14:45 280e9fcd

fix(Tactic/FunProp): do not unfold semireducible definitions in the presence of projections (#35548) Currently, fun_prop incorrectly unfolds semireducible definitions when a projection or recursor is applied. This PR fixes this by switching to whnfR together with Lean.Meta.withCanUnfoldPred for the custom unfolding logic. Unfortunately, there are many proofs which rely on this bug. To avoid breaking proofs, the option fun_prop.projDefaultTransparency is added for locally restoring the previous behavior. Removing the uses of this option is left for future PRs. See #mathlib4 > two fun_prop failures @ 💬 for an example where this bug caused issues in Physlib.