Port to leanprover/lean4:v4.26.0

[ovo-Tim]

Close #105

Dependencies (lakefile.lean)

• Updated GameServer branch: bump-v4.23.0 → chore/bump-v4.26.0
• Updated mathlib: from hrmacbeth/mathlib4 fork → official leanprover-community/mathlib4 at v4.26.0

Tactic API change (Game/CustomTactic/Linarith.lean)

• Added import Mathlib.Util.ElabWithoutMVars
• Replaced deprecated elabLinarithArg with elabTermWithoutNewMVars

Missing import (Game/Metadata.lean)

• Uncommented import Mathlib.Tactic.Cases (needed for cases' tactic)

Theorem rename: abs_add → abs_add_le (across 20+ files)

• Bulk replaced all occurrences of apply abs_add with apply abs_add_le
• Also updated TheoremDoc, NewTheorem, and introduction text references

Tactic fixes in Game/Levels/L4Levels/L01_NonConverge.lean

• norm_num → (abs_of_pos two_pos).symm for 2 = |2| proof
• ring_nf → congr 1; ring for absolute value equality proofs

Tactic fixes in Game/Levels/L4Pset/L4Pset1.lean

• Same pattern: norm_num → (abs_of_pos two_pos).symm and ring_nf → congr 1; ring for absolute value proofs

[jcreedcmu]

Looks good to me, except I think we can remove the .claude and Game.pot changes.

[AlexKontorovich]

Thanks!