Add induction on partizan games

[emmett-w]

I think I might need an edit to the discouraged file, but I'm not sure how to do that on MacOS. All the changes are just within my mathbox though.

[avekens]

I think I might need an edit to the discouraged file, but I'm not sure how to do that on MacOS. All the changes are just within my mathbox though.

The discouraged file should not be added by hand, but generated automatically. I do this with mmj2.
However, I wonder why you tagged some of your theorems with "New usage is discouraged.". Since they are in a mathbox, they can be used only in this mathbox anyway.

[emmett-w]

Thank you - how do I generate the discouraged file with mmj2 on a Mac? I added the discouragement tag to a theorem that's a weaker technical lemma to the following theorem.

[icecream17]

One option is to use an online service such as github codespaces https://github.com/codespaces/new where you can run commands on a linux machine through the internet

(note: When I tested the link it mentions "paid for by", but the default spending limit is 0$ and I dont reach the limit unless I take hours)

[emmett-w]

I updated the discouraged file so it should be good now. Is this ready to merge?

[avekens]

OK, this is not named as lemma, but it seems to be a lemma for ~pgind. So the remarks on ~ pgindlem apply also for this theorem.

[emmett-w]

Yes, that's what I intended. Is there anything I need to add or change about the file?

[emmett-w]

Is everything ready to merge?

[sctfn]

You appear to still have merge conflicts. What is Github reporting for your merge?

[emmett-w]

You appear to still have merge conflicts. What is Github reporting for your merge?

I'm not so experienced with git so I don't understand exactly what you're referring to. There's a message saying
"This branch has conflicts that must be resolved
Only those with write access to this repository can merge pull requests.
Conflicting files

discouraged
set.mm

"

There's a greyed out button next to it saying resolve conflicts

[icecream17]

The from-branch https://github.com/emmett-w/set.mm/tree/pginduction is 4164 commits behind this one. The message means there are conflicts between the from-branch and the 4164 commits

Since there are so many intermediate commits, probably the easiest thing to do is to make a new updated branch and do the commits again.
(https://github.com/emmett-w/set.mm/branches > "New branch" > change the Source to metamath/set.mm > "Create new branch")

[icecream17]

The merge was successfully done 🎉 (Diff of effective changes to set.mm/develop) between 2nd and 4th commit:

discouraged
@@ -> 3252 @@
+ "cbvralv2" is used by "pgindnf".
@@ -> 15373 @@
+ New usage of "cbvralv2" is discouraged (1 uses).

(There's probably a replacement for cbvralv2 somewhere but I can't find it. But pgindnf will probably be changed in the future to use the replacement)

[emmett-w]

The merge was successfully done 🎉 (Diff of effective changes to set.mm/develop) between 2nd and 4th commit:

discouraged
@@ -> 3252 @@
+ "cbvralv2" is used by "pgindnf".
@@ -> 15373 @@
+ New usage of "cbvralv2" is discouraged (1 uses).

(There's probably a replacement for cbvralv2 somewhere but I can't find it. But pgindnf will probably be changed in the future to use the replacement)

Thank you!