M : Type ?u.118917
N : Type ?u.118920
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_1
H : Type ?u.118932
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
M : Type ?u.118917
N : Type ?u.118920
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_1
H : Type ?u.118932
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
haveI := Fintype.ofFinite s
M : Type ?u.118917
N : Type ?u.118920
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_1
H : Type ?u.118932
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure ↑(Set.toFinset s) } ≤ Finset.card (Set.toFinset s)
M : Type ?u.118917
N : Type ?u.118920
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_1
H : Type ?u.118932
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
no goals
M : Type ?u.118917
N : Type ?u.118920
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_1
H : Type ?u.118932
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure ↑(Set.toFinset s) } ≤ Finset.card (Set.toFinset s)
exact rank_closure_finset_le_card s.toFinset