[Merged by Bors] - chore: work around simp issues in future nightlies #11546
Conversation
Ruben-VandeVelde
commented
Mar 20, 2024
Ruben-VandeVelde
commented
Ruben-VandeVelde
added
the
awaiting-review
| @@ -185,11 +185,13 @@ def toPreimages : J ⥤ Type v where | |||
| rw [← mem_preimage, preimage_preimage, mem_preimage] | |||
| convert h (g ≫ f); rw [F.map_comp]; rfl | |||
| map_id j := by | |||
| simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_id] | |||
| -- Adaptation note: nightly-2024-03-16: simp [Subtype.map] | |||
There was a problem hiding this comment.
If we're going to write an adaptation note, I think we ought to mention that unfoldPartialApp was removed.
There was a problem hiding this comment.
If the new simp only doesn't have any downsides (e.g. apparently here?), I think just delete the adaptation note.
If there is some downside, the adaptation note should contain enough information for someone coming along afterwards to reconstruct the original proof and see if it works again.
There was a problem hiding this comment.
The downside is that we need to add those _def lemmas at all, and remember when to use them rather than the name of the definition itself, so I've opted to clarify the comments. If we decide to stay with the new code, they're easy to find and remove.
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
