case intro.intro
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ f x ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
⊢ f '' closure s ≤ closure (f '' s)
rintro _ ⟨x, hx, rfl⟩
no goals
case intro.intro
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ f x ∈ closure (f '' s)
exact InClosure.recOn hx
  (by intros _ ha; exact subset_closure (mem_image_of_mem f ha))
  (by
    rw [hf.map_one]
    apply IsSubmonoid.one_mem (closure.isSubgroup _).toIsSubmonoid)
  (by
    intros _ _
    rw [hf.map_inv]
    apply IsSubgroup.inv_mem (closure.isSubgroup _))
  (by
    intros _ _ _ _ ha hb
    rw [hf.map_mul]
    exact (closure.isSubgroup (f '' s)).toIsSubmonoid.mul_mem ha hb)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝ : G
ha : a✝ ∈ s
⊢ f a✝ ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a : G}, a ∈ s → f a ∈ closure (f '' s)
intros _ ha
no goals
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝ : G
ha : a✝ ∈ s
⊢ f a✝ ∈ closure (f '' s)
exact subset_closure (mem_image_of_mem f ha)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ 1 ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ f 1 ∈ closure (f '' s)
rw [hf.map_one]
no goals
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ 1 ∈ closure (f '' s)
apply IsSubmonoid.one_mem (closure.isSubgroup _).toIsSubmonoid
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → f a✝¹⁻¹ ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a : G}, InClosure s a → f a ∈ closure (f '' s) → f a⁻¹ ∈ closure (f '' s)
intros _ _
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → (f a✝¹)⁻¹ ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → f a✝¹⁻¹ ∈ closure (f '' s)
rw [hf.map_inv]
no goals
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → (f a✝¹)⁻¹ ∈ closure (f '' s)
apply IsSubgroup.inv_mem (closure.isSubgroup _)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f (a✝² * b✝) ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a b : G},
    InClosure s a → InClosure s b → f a ∈ closure (f '' s) → f b ∈ closure (f '' s) → f (a * b) ∈ closure (f '' s)
intros _ _ _ _ ha hb
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f a✝² * f b✝ ∈ closure (f '' s)
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f (a✝² * b✝) ∈ closure (f '' s)
rw [hf.map_mul]
no goals
G : Type u_2
H : Type u_1
A : Type ?u.130329
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f a✝² * f b✝ ∈ closure (f '' s)
exact (closure.isSubgroup (f '' s)).toIsSubmonoid.mul_mem ha hb