M : Type ?u.71766
N : Type ?u.71769
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.71781
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid ↔ AddSubmonoid.FG (↑toAddSubgroup P).toAddSubmonoid
M : Type ?u.71766
N : Type ?u.71769
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.71781
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ AddSubgroup.FG (↑toAddSubgroup P)
rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
no goals
M : Type ?u.71766
N : Type ?u.71769
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.71781
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid ↔ AddSubmonoid.FG (↑toAddSubgroup P).toAddSubmonoid
exact (Subgroup.toSubmonoid P).fg_iff_add_fg