case mk.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.149443
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.149464
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.149488
mc : MonoidHomClass F M N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, ↑(submonoidMap f M') a = { val := ↑f x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f x) }
M : Type u_1
N : Type u_2
P : Type ?u.149443
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.149464
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.149488
mc : MonoidHomClass F M N
f : M →* N
M' : Submonoid M
⊢ Function.Surjective ↑(submonoidMap f M')
rintro ⟨_, x, hx, rfl⟩
no goals
case mk.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.149443
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.149464
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.149488
mc : MonoidHomClass F M N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, ↑(submonoidMap f M') a = { val := ↑f x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f x) }
exact ⟨⟨x, hx⟩, rfl⟩