no goals
M : Type u_2
N : Type ?u.12734
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
classical
  obtain ⟨s, rfl⟩ := h
  exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
case intro
M : Type u_2
N : Type ?u.12734
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ FG (Submonoid.map e (closure ↑s))
M : Type u_2
N : Type ?u.12734
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
obtain ⟨s, rfl⟩ := h
no goals
case intro
M : Type u_2
N : Type ?u.12734
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ FG (Submonoid.map e (closure ↑s))
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
no goals
M : Type u_2
N : Type ?u.12734
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (↑e) s) = Submonoid.map e (closure ↑s)
rw [Finset.coe_image, MonoidHom.map_mclosure]