Theorem: Subgroup.map_commutator_eq (Jordan/Mathlib/Commutators.lean)

State before:
G✝ : Type ?u.2272
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
⊢ map f (_root_.commutator H) = ⁅MonoidHom.range f, MonoidHom.range f⁆
Tactic:
rw [_root_.commutator_def, Subgroup.map_commutator, Subgroup.map_top_eq_range]
State after:
no goals