Commit 2025-12-04 09:22 8101f86b

View on Github →

feat(Tactic): add lia as an alias for cutsat and use it throughout (#32376)

Summary

Test plan

  • Verified core tactic files build (Mathlib.Tactic.Lia, Mathlib.Tactic.Common)
  • Verified linter tests pass (MathlibTest.FlexibleLinter, MathlibTest.TacticAnalysis)
  • CI will run full build 🤖 Prepared with Claude Code

Estimated changes

modified theorem Nat.succ_mod_two_eq_one_iff
modified theorem sq_eq_one
modified def Matrix.vecAlt0
modified theorem Int.lt_succ_self
modified theorem Int.pred_self_lt
modified theorem Int.toNat_lt_of_ne_zero
modified theorem Multiset.coe_mem
modified theorem NeZero.one_le
modified theorem Nat.cast_nonpos
modified theorem Nat.dist_eq_sub_of_le
modified theorem Nat.dist_eq_zero
modified theorem Nat.dist_pos_of_ne
modified theorem Nat.dist_succ_succ
modified theorem Nat.dist_tri_left'
modified theorem Nat.dist_tri_left
modified theorem Nat.dist_tri_right'
modified theorem Nat.dist_tri_right
modified theorem Nat.dist_zero_left
modified theorem Nat.dist_zero_right
modified theorem Nat.eq_of_dist_eq_zero
modified theorem List.Vector.get_tail
modified theorem finRotate_last'
modified theorem Nat.fermatNumber_ne_one