theorem Subgroup.closure_submonoid {G : Type u_1} [CommGroup G] (N : Submonoid G) : ↑(Subgroup.closure ↑N) = {x : G | ∃ (a : ↥N) (b : ↥N), x = ↑a * (↑b)⁻¹}

theorem AddSubgroup.closure_addSubmonoid {G : Type u_1} [AddCommGroup G] (N : AddSubmonoid G) : ↑(AddSubgroup.closure ↑N) = {x : G | ∃ (a : ↥N) (b : ↥N), x = ↑a + -↑b}

theorem AddGroup.exists_finite_generating_set_of_FG (M : Type u_2) [AddCommGroup M] [AddGroup.FG M] (s : Set M) (h : AddSubgroup.closure s = ⊤) : ∃ (t : Finset M), ↑t ⊆ s ∧ AddSubgroup.closure ↑t = ⊤

theorem AddGroup.exists_finite_generating_set_of_FG' (M : Type u_2) [AddCommGroup M] (s : Set M) (h : AddGroup.FG ↥(AddSubgroup.closure s)) : ∃ (t : Finset M), ↑t ⊆ s ∧ AddSubgroup.closure ↑t = AddSubgroup.closure s

instance AddGroup.instFGProd_project (M : Type u_2) (N : Type u_3) [AddCommGroup M] [AddCommGroup N] [AddGroup.FG M] [AddGroup.FG N] : AddGroup.FG (M × N)

theorem Subgroup.FG.map {A : Type u_2} {B : Type u_3} [Group A] [Group B] {S : Subgroup A} (h : S.FG) (f : A →* B) : (Subgroup.map f S).FG

theorem AddSubgroup.FG.map {A : Type u_2} {B : Type u_3} [AddGroup A] [AddGroup B] {S : AddSubgroup A} (h : S.FG) (f : A →+ B) : (AddSubgroup.map f S).FG

theorem Submonoid.mem_closure_iff (M : Type u_2) [CommMonoid M] (S : Set M) (x : M) : x ∈ Submonoid.closure S ↔ ∃ (n : M →₀ ℕ) (_ : ∀ i ∈ n.support, i ∈ S), (n.prod fun (y : M) (i : ℕ) => y ^ i) = x