G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
haveI := H.fG_of_index_ne_zero
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
T : Finset { x // x ∈ H }
hT₀ : Finset.card T ≤ index H * Finset.card S
hT : closure ↑T = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS