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