New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: remove Equiv.toFun_as_coe_apply
#7902
Conversation
-- porting note: `simp` should prove this using `toFun_as_coe`, but it doesn't. | ||
-- This might be a bug in `simp` -- see https://github.com/leanprover/lean4/issues/1937 | ||
-- If this issue is fixed then the simp linter probably will start complaining, and | ||
-- this theorem can be deleted hopefully without breaking any `simp` proofs. | ||
@[simp] theorem toFun_as_coe_apply (e : α ≃ β) (x : α) : e.toFun x = e x := rfl | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why doesn't simpNF
complain about this one?
Equiv.toFun_as_coe_apply
bors merge I tweaked the title to include the name of the lemma |
This `simp` lemma was added during the port but tagged as probably unnecessary after fixing leanprover/lean4#1937. This PR confirms it is indeed no longer necessary. The only proofs that needed fixing were the one explicitly calling the new simp lemma. The porting note can go too.
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Equiv.toFun_as_coe_apply
Equiv.toFun_as_coe_apply
This
simp
lemma was added during the port but tagged as probably unnecessary after fixing leanprover/lean4#1937. This PR confirms it is indeed no longer necessary. The only proofs that needed fixing were the one explicitly calling the new simp lemma.The porting note can go too.