G : Type u_3
G' : Type ?u.474061
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.474070
inst✝² : AddGroup A
N : Type u_1
P : Type u_2
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (comp g f) ⊤
G : Type u_3
G' : Type ?u.474061
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.474070
inst✝² : AddGroup A
N : Type u_1
P : Type u_2
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
g : N →* P
f : G →* N
⊢ map g (range f) = range (comp g f)
rw [range_eq_map, range_eq_map]
no goals
G : Type u_3
G' : Type ?u.474061
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.474070
inst✝² : AddGroup A
N : Type u_1
P : Type u_2
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (comp g f) ⊤
exact (⊤ : Subgroup G).map_map g f