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

State before:
G✝ : Type ?u.1324
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
⊢ map f ⊤ = MonoidHom.range f
Tactic:
simp only [map_eq_range_iff, codisjoint_top_left]
State after:
no goals