Union of proper submodules is proper subset

Stream: Is there code for X?

[Oliver Nash]

Does anyone happen to have a proof of this lying around:

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Module.Submodule.Lattice
import Mathlib.Data.Finite.Defs

lemma Submodule.exists_forall_notMem_of_forall_ne_top
    {ι K M : Type*} [Finite ι] [Field K] [Infinite K] [AddCommGroup M] [Module K M]
    (p : ι → Submodule K M) (h : ∀ i, p i ≠ ⊤) :
    ∃ x, ∀ i, x ∉ p i := by
  sorry

[Oliver Nash]

I note that various stronger forms exist (see e.g., this MO question or this MO question but IMHO this statement would be worth a PR in its own right.

[Oliver Nash]

I must also confess this is more of an attempt at nerd-sniping than an honest query, but I think it might be a fun bite-sized exercise for someone.

[Oliver Nash]

(In case anyone ever returns to this thread: this became my last sorry so I closed it myself in #27598.)