Commit 2025-02-25 18:31 73d6d99b
View on Github →refactor(CategoryTheory/ConcreteCategory): concreteify NatTrans.naturality_apply (#22275)
This lemma was still stated using HasForget, we can turn it into taking ConcreteCategory for some nice downstream cleanup.