Commit 2026-09-26 09:19 a98628e1

View on Github →

chore: use congr() much more widely (#43408) Replace most uses of congr_fun, congr_arg, DFunLike.congr_fun, DFunLike.congr_arg, etc... by uses of the congr() elaborator. Some uses were silly and have been replaced by the congr or congr! tactic? Generated by Claude Opus, painstakingly reviewed and improved line-by-line by myself. Assisted-by: Claude Opus 5

Estimated changes

modified theorem Counterexample.B_ne_zero
modified theorem iterate_frobenius
modified theorem LinearEquiv.pow_apply
modified theorem Module.End.pow_apply
modified theorem PiLp.norm_ofLp
modified theorem CategoryTheory.eqToHom_op
modified theorem IsBaseChange.finrank_eq
modified theorem measurable_eq_mp