Theorem: Subgroup.commutator_eq' (Jordan/Mathlib/Commutators.lean)

State before:
G✝ : Type ?u.3265
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map (Subgroup.subtype H) (_root_.commutator ↥H) = ⁅H, H⁆
Tactic:
simp only [map_commutator_eq, subtype_range]
State after:
no goals