[Merged by Bors] - feat(SetTheory/Game/PGame): inserting an option a game

[hwatheod]

inserting an option into a game

---

This PR is split out of #14498. Here, we define the operation of inserting a left or right option into a game, and prove a few standard results about it.

[github-actions]

PR summary 1e4fe08ef0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ insertLeft
+ insertLeft_equiv_of_lf
+ insertLeft_numeric
+ insertRight
+ insertRight_equiv_of_lf
+ insertRight_insertLeft
+ insertRight_le
+ insertRight_numeric
+ le_insertLeft
+ neg_insertLeft_neg
+ neg_insertRight_neg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[eric-wieser]

I think this is about as far as I can review this, as someone not that familiar in the area. The style and naming looks good now, thanks. I'll have a quick go at shortening the proofs, but probably someone else should give this the final review to check if any obvious lemmas are missing.

[hwatheod]

I moved insertLeft_numeric and insertRight_numeric to a position after Numeric.neg so I could use Numeric.neg to write the proof of insertRight_numeric in terms of insertLeft_numeric (like @eric-wieser did for the other file)

[eric-wieser]

Any reason to not instead use

Suggested change

	| mk xl xr xL xR => mk (xl ⊕ PUnit) xr (Sum.elim xL fun _ => x') xR
	| mk xl xr xL xR => mk (Option xl) xr (Option.rec x' xL) xR

or whatever the spelling is that works?

[eric-wieser]

This nicely avoids having any useless _ : Unit variables floating around

[hwatheod]

I'm not sure about this. First, the proof of insertLeft_numeric seems to get a little more complicated, since simp doesn't seem to work very well with Option values and I have to do an additional layer of constructor / rcases. But also, perhaps more significantly, this wouldn't generalize to the case where we want to insert a whole family xl' -> PGame, in which case we definitely need a xl ⊕ xl'. I think we would want to do that later in the development of the theory.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style