!4#2424

Stream: PR reviews

[Scott Morrison]

@Adam Topaz, I've proposed a fix for the simpNF linter issue in your !4#2424 PR (the simp lemmas aren't actually needed: remove them). Could you have a look and see if you're happy with my commit there?

[Adam Topaz]

Thanks Scott! To be honest, I forgot that I still had this PR open (I need to get my github notifications under control...). I'll go through it now.

[Adam Topaz]

Given the success of the backport PR, it seems that we can also remove the lemmas adjointOfOpAdjointOp_homEquiv_apply and adjointOfOpAdjointOp_homEquiv_symm_apply that were added manually by @Matthew Ballard (and modified by @Scott Morrison ). Are you both happy with that?

[Matthew Ballard]

They were mindlessly added by me so :thumbs_up:

[Adam Topaz]

Okay, I'll go ahead and remove them.

[Adam Topaz]

anyway, if we want/need to add them back later, we can do so easily using this diff: https://github.com/leanprover-community/mathlib4/pull/2424/commits/de6fba10de6ecbca2baa5f177e804e34c082525b