-- Mathlib/GroupTheory/Finiteness.lean
theorem Submonoid.FG.map_injective {M' : Type*} [Monoid M'] {P : Submonoid M} (e : M →* M')
    (he : Function.Injective e) (h : (P.map e).FG) : P.FG

Proof state:
case h.a.e_s
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤

Tactic:
exact Submonoid.monotone_map le_top

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ P.FG

Tactic:
use s.preimage e he.injOn

Result:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(s.preimage ⇑e ⋯) = P

Proof state:
case h.a
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e (closure ↑(s.preimage ⇑e ⋯)) = Submonoid.map e P

Tactic:
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]

Result:
case h.a
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (⇑e '' (⇑e ⁻¹' ↑s)) = closure ↑s

Proof state:
case h.a.e_s
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ ⇑e '' (⇑e ⁻¹' ↑s) = ↑s

Tactic:
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
    MonoidHom.mrange_eq_map e]

Result:
case h.a.e_s
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤

Proof state:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(s.preimage ⇑e ⋯) = P

Tactic:
apply Submonoid.map_injective_of_injective he

Result:
case h.a
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e (closure ↑(s.preimage ⇑e ⋯)) = Submonoid.map e P

Proof state:
case h.a
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (⇑e '' (⇑e ⁻¹' ↑s)) = closure ↑s

Tactic:
congr

Result:
case h.a.e_s
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ ⇑e '' (⇑e ⁻¹' ↑s) = ↑s

Proof state:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
h : (Submonoid.map e P).FG
⊢ P.FG

Tactic:
obtain ⟨s, hs⟩ := h

Result:
case intro
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ P.FG