Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 08:32 1fbe1183

View on Github →

golf(set_theory/game/pgame): golf neg_le_neg_iff (#14726) Also in this PR:

  • slightly golf subsequent.trans
  • replace -> by →
  • replace a nonterminal simp by dsimp

Estimated changes

modified theorem pgame.left_moves_add_cases
modified theorem pgame.neg_le_neg_iff
modified theorem pgame.neg_lf_neg_iff
modified theorem pgame.right_moves_add_cases
modified theorem pgame.subsequent.trans