[Merged by Bors] - feat: port SetTheory.Game.Basic

[QuinnLesquimau]

---

[urkud]

There was no activity here for ~2 weeks, so I assume that you are not actively working on this PR. I'll add help-wanted so that anyone can contribute without an explicit permission from the author.

[dwrensha]

I got quot_left_distrib and quot_mul_assoc working. Now the only remaining task I see is to resolve some simpNF linter issues.

[semorrison]

@Parcly-Taxel the new lemmas you just added, e.g.

@[simp]
theorem neg_mk_mul_moveLeft_inl' {xl xr yl yr} {xL xR yL yR} {i j} :
    -(mk xl xr xL xR * mk yl yr yL yR).moveRight
    (@FunLike.coe _ _ (fun _ => RightMoves (mk xl xr xL xR * mk yl yr yL yR))
      Equiv.instFunLikeEquiv toLeftMovesNeg.symm (Sum.inl (i, j))) =
    -(xL i * mk yl yr yL yR + mk xl xr xL xR * yR j - xL i * yR j) :=
  rfl

seem unlikely to be useful to me. At least for this file, we don't need them. Could you either:

• remove them
• working out how to reformulate them in some way that is still useful, but doesn't have @FunLike.coe?

[Parcly-Taxel]

@Parcly-Taxel the new lemmas you just added, e.g.

@[simp]
theorem neg_mk_mul_moveLeft_inl' {xl xr yl yr} {xL xR yL yR} {i j} :
    -(mk xl xr xL xR * mk yl yr yL yR).moveRight
    (@FunLike.coe _ _ (fun _ => RightMoves (mk xl xr xL xR * mk yl yr yL yR))
      Equiv.instFunLikeEquiv toLeftMovesNeg.symm (Sum.inl (i, j))) =
    -(xL i * mk yl yr yL yR + mk xl xr xL xR * yR j - xL i * yR j) :=
  rfl

seem unlikely to be useful to me. At least for this file, we don't need them. Could you either:

* remove them

* working out how to reformulate them in some way that is still useful, but doesn't have `@FunLike.coe`?

I don't know how to get the FunLike.coe out –

toRightMovesNeg.symm (Sum.inr (i, j))

as shown in the infoview doesn't work. But there has to be a way to do so.

[semorrison]

should say why, please: "simpNF linter complains".

[semorrison]

(and below)

[semorrison]

Okay, I've created a lean4 issue for the termination_by problem (or at least something closely related?).

@Parcly-Taxel, if you could just fix the porting notes then I think we can merge.

[Parcly-Taxel]

@semorrison OK, done.

[semorrison]

Bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style