[Merged by Bors] - refactor(set_theory/game/pgame): tweak relabelling definition
#14941
Conversation
vihdzp
added
the
awaiting-review
| { apply equiv.equiv_punit }, | ||
| { apply equiv.equiv_pempty }, | ||
| { simp } | ||
| refine ⟨_, _, λ i, _, is_empty.elim _⟩, |
There was a problem hiding this comment.
There's a bit of a regression here, as for whatever reason Lean is now unable to see through some quite dense def-eqs. But given how particularly messy this proof is, I wouldn't worry much.
|
I've changed this PR to use @alreadydone's suggestion for Also, I've added some basic API on destructuring relabellings, since it allows for even more golfing. |
src/set_theory/game/pgame.lean
Outdated
| @[refl] def relabelling.refl : Π (x : pgame), x ≡r x | ||
| | ⟨xl, xr, xL, xR⟩ := ⟨equiv.refl _, equiv.refl _, λ i, relabelling.refl _, λ j, relabelling.refl _⟩ | ||
| @[refl] def refl : Π (x : pgame), x ≡r x | ||
| | x := ⟨equiv.refl _, equiv.refl _, λ i, refl _, λ j, refl _⟩ | ||
| using_well_founded { dec_tac := pgame_wf_tac } |
There was a problem hiding this comment.
This type of cleanup is independent of the change to the definition of relabelling, right? If so, would you mind splitting out the remove-⟨xl, xr, xL, xR⟩ and namespace relabelling part of this change, just to make it easier to evaluation what the advantage of removing the .symm is?
Feel free to tag me in the split PR / zulip / discord to get a quick review.
There was a problem hiding this comment.
Sure, I'll put that elsewhere.
mathlib-dependent-issues-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
|
bors r+ |
github-actions
bot
added
ready-to-merge
We simplify the definition for a `relabelling` by using `R` instead of `R.symm`. This overall leads to more symmetric proofs. We also create a constructor with the equivalences swapped. This allows us to golf various theorems. Further, we add basic API on destructuring relabellings, which makes it so that we don't have to case on them all the time.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
relabelling definitionrelabelling definition
We simplify the definition for a `relabelling` by using `R` instead of `R.symm`. This overall leads to more symmetric proofs. We also create a constructor with the equivalences swapped. This allows us to golf various theorems. Further, we add basic API on destructuring relabellings, which makes it so that we don't have to case on them all the time.
We simplify the definition for a
relabellingby usingRinstead ofR.symm. This overall leads to more symmetric proofs.We also create a constructor with the equivalences swapped. This allows us to golf various theorems.
Further, we add basic API on destructuring relabellings, which makes it so that we don't have to case on them all the time.