minimize_imports and lazily generated equation lemmas

Stream: general

[Ruben Van de Velde]

I just debugged a case where minimize_imports suggested keeping an import because it got Prod.swap.eq_1 from there - can we make it smarter in cases like that?

[Damiano Testa]

Does it have a ! flag?

[Ruben Van de Velde]

No

[Kim Morrison]

It does certainly seem possible. We need to update Environment.getModuleFor? in ImportGraph/RequiredModules.lean in the import-graph repository.