no goals
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
classical
  obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
  use s.image f
  rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
    MonoidHom.mrange_top_iff_surjective]
case intro
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset ?m.53983
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
case intro
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (↑f) s) = ⊤
case intro
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset ?m.53983
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'
use s.image f
no goals
case intro
M : Type u_2
N : Type ?u.44817
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_1
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (↑f) s) = ⊤
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
  MonoidHom.mrange_top_iff_surjective]