M : Type u_1
N✝ : Type ?u.43187
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG (Submonoid.map (Submonoid.subtype N) ⊤)
M : Type u_1
N✝ : Type ?u.43187
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG N
conv_rhs => rw [← N.range_subtype, MonoidHom.mrange_eq_map]
no goals
M : Type u_1
N✝ : Type ?u.43187
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG (Submonoid.map (Submonoid.subtype N) ⊤)
exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩