no goals
M : Type u_1
N : Type ?u.2057
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : FG P
S : Set M
hS : closure S = P
hf : Set.Finite S
⊢ AddSubmonoid.closure (↑Additive.toMul ⁻¹' S) = ↑toAddSubmonoid P
simp [← Submonoid.toAddSubmonoid_closure, hS]
no goals
M : Type u_1
N : Type ?u.2057
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : AddSubmonoid.FG (↑toAddSubmonoid P)
T : Set (Additive M)
hT : AddSubmonoid.closure T = ↑toAddSubmonoid P
hf : Set.Finite T
⊢ closure (↑Multiplicative.ofAdd ⁻¹' T) = P
simp [← AddSubmonoid.toSubmonoid'_closure, hT]