Commit 2025-07-19 04:00 59d8ae47

View on Github →

feat(Algebra): add Aesop automation around Even / IsSquare (#26177)

  • Add aesop attributes to enable automation for goals of the form Even x, IsSquare x and IsSumSq x
  • Add test examples
  • Replace some existing proofs with by aesop The automation follows the principles of #25961 (see the file Mathlib/Tactic/SetLike.lean for documentation).

Estimated changes

modified theorem Even.isSquare_pow
modified theorem IsSquare.mul
modified theorem IsSquare.mul_self
modified theorem IsSquare.pow
modified theorem IsSquare.zpow
modified theorem IsSquare.isSumSq
added theorem IsSumSq.sum_sq