no goals
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
s : Finset ι
N : ι → Submodule R M
h : ∀ (i : ι), i ∈ s → FG (N i)
⊢ FG (⨆ (i : ι) (_ : i ∈ s), N i)
simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h