no goals
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ f 1 ∈ s
(rw [IsMonoidHom.map_one hf]; exact hs.one_mem)
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ 1 ∈ s
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ f 1 ∈ s
rw [IsMonoidHom.map_one hf]
no goals
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ 1 ∈ s
exact hs.one_mem
no goals
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f (a * b) ∈ s
(rw [IsMonoidHom.map_mul' hf]; exact hs.mul_mem ha hb)
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f a * f b ∈ s
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f (a * b) ∈ s
rw [IsMonoidHom.map_mul' hf]
no goals
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.24553
inst✝¹ : AddMonoid A
t : Set A
N : Type u_1
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f a * f b ∈ s
exact hs.mul_mem ha hb