case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card (↑↑S → ↑(commutatorSet G))
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
no goals
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card (↑↑S → ↑(commutatorSet G))
exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)