minImports missing imports from Init

Stream: mathlib4

[Daniel Weber]

I don't have a minimal example, but in #16797 in Mathlib/FieldTheory/Differential/Basic.lean, linter.minImports says:

warning: ././././Mathlib/FieldTheory/Differential/Basic.lean:6:0: -- missing imports
import Init.Data.ULift
import Init.Data.Fin.Fold
import Init.Data.List.Nat.Pairwise

What is that supposed to mean?

[Damiano Testa]

I think that this might be the same as

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60minImports.60.20thinks.20.60Finsupp.2Esupport.60.20is.20.60Function.2Esupport.60.3F/near/480462205

I think that there is something going on with Init imports in ImportGraph, but have not gotten to the bottom of it.