case intro.intro
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
hx : x ∈ Closure s
⊢ f x ∈ Closure (f '' s)
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
⊢ f '' Closure s ≤ Closure (f '' s)
rintro _ ⟨x, hx, rfl⟩
case intro.intro.basic
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x z : M
hz : z ∈ s
⊢ f z ∈ Closure (f '' s)

case intro.intro.one
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ f 1 ∈ Closure (f '' s)

case intro.intro.mul
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f (a✝² * b✝) ∈ Closure (f '' s)
case intro.intro
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
hx : x ∈ Closure s
⊢ f x ∈ Closure (f '' s)
induction' hx with z hz
no goals
case intro.intro.basic
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x z : M
hz : z ∈ s
⊢ f z ∈ Closure (f '' s)
solve_by_elim [subset_closure, Set.mem_image_of_mem]
case intro.intro.one
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ 1 ∈ Closure (f '' s)
case intro.intro.one
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ f 1 ∈ Closure (f '' s)
rw [hf.map_one]
no goals
case intro.intro.one
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ 1 ∈ Closure (f '' s)
apply IsSubmonoid.one_mem (closure.isSubmonoid (f '' s))
case intro.intro.mul
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f a✝² * f b✝ ∈ Closure (f '' s)
case intro.intro.mul
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f (a✝² * b✝) ∈ Closure (f '' s)
rw [hf.map_mul]
no goals
case intro.intro.mul
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A✝ : Type ?u.63949
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_1
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f a✝² * f b✝ ∈ Closure (f '' s)
solve_by_elim [(closure.isSubmonoid _).mul_mem]