case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ map (Subgroup.subtype (closure s)) (closure (↑(Subgroup.subtype (closure s)) ⁻¹' s)) =
    map (Subgroup.subtype (closure s)) ⊤
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ closure (↑(Subgroup.subtype (closure s)) ⁻¹' s) = ⊤
apply map_injective (closure s).subtype_injective
case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ s ⊆ Set.range ↑(Subgroup.subtype (closure s))
case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ map (Subgroup.subtype (closure s)) (closure (↑(Subgroup.subtype (closure s)) ⁻¹' s)) =
    map (Subgroup.subtype (closure s)) ⊤
rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, subtype_range,
  Set.image_preimage_eq_of_subset]
case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ s ⊆ {x | x ∈ ↑(closure s)}
case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ s ⊆ Set.range ↑(Subgroup.subtype (closure s))
rw [coeSubtype, Subtype.range_coe_subtype]
no goals
case a
G : Type u_1
G' : Type ?u.604785
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.604794
inst✝¹ : AddGroup A
N : Type ?u.604800
inst✝ : Group N
f : G →* N
s : Set G
⊢ s ⊆ {x | x ∈ ↑(closure s)}
exact subset_closure