case h.a
M : Type u_1
N : Type u_2
P : Type ?u.176338
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.176359
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
e : M ≃* N
x✝ : { x // x ∈ S }
⊢ ↑(↑(equivMapOfInjective S ↑e (_ : Function.Injective ↑e)) x✝) = ↑(↑(MulEquiv.submonoidMap e S) x✝)
M : Type u_1
N : Type u_2
P : Type ?u.176338
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.176359
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
e : M ≃* N
⊢ equivMapOfInjective S ↑e (_ : Function.Injective ↑e) = MulEquiv.submonoidMap e S
ext
no goals
case h.a
M : Type u_1
N : Type u_2
P : Type ?u.176338
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.176359
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
e : M ≃* N
x✝ : { x // x ∈ S }
⊢ ↑(↑(equivMapOfInjective S ↑e (_ : Function.Injective ↑e)) x✝) = ↑(↑(MulEquiv.submonoidMap e S) x✝)
rfl