case intro.intro
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ rank G
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ rank G' ≤ rank G
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ Finset.card (Finset.image (↑f) S)

M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Finset.card (Finset.image (↑f) S) ≤ rank G
case intro.intro
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ rank G
trans (S.image f).card
case hS
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (↑f) S) = ⊤
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ Finset.card (Finset.image (↑f) S)
apply Group.rank_le
no goals
case hS
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (↑f) S) = ⊤
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
no goals
M : Type ?u.90865
N : Type ?u.90868
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_1
H : Type ?u.90880
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_2
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Finset.card (Finset.image (↑f) S) ≤ rank G
exact Finset.card_image_le.trans_eq hS1