case intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), FG (N i)
val✝ : Fintype ι
⊢ FG (iSup N)
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), FG (N i)
⊢ FG (iSup N)
cases nonempty_fintype ι
no goals
case intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), FG (N i)
val✝ : Fintype ι
⊢ FG (iSup N)
simpa using fg_biSup Finset.univ N fun i _ => h i