case intro
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ FG P
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
h : FG (Submonoid.map e P)
⊢ FG P
obtain ⟨s, hs⟩ := h
case intro
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s))) = P
case intro
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ FG P
use s.preimage e (he.injOn _)
case intro.a
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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 ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s)))) = Submonoid.map e P
case intro
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s))) = P
apply Submonoid.map_injective_of_injective he
case intro.a
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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
case intro.a
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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 ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s)))) = Submonoid.map e P
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
case intro.a.e_s
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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
case intro.a
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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
congr
case intro.a.e_s
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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 ⊤
case intro.a.e_s
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
    MonoidHom.mrange_eq_map e]
no goals
case intro.a.e_s
M : Type u_2
N : Type ?u.23387
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_1
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 ⊤
exact Submonoid.monotone_map le_top