case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : Set.Finite t'
⊢ FG (span R t')
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, Set.Finite S ∧ span R S = N) → FG N
rintro ⟨t', h, rfl⟩
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Finset M
h : Set.Finite ↑t
⊢ FG (span R ↑t)
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : Set.Finite t'
⊢ FG (span R t')
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
no goals
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Finset M
h : Set.Finite ↑t
⊢ FG (span R ↑t)
exact ⟨t, rfl⟩