[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
x✝ : ∃ S, closure S = P ∧ Set.Finite S
S : Set M
hS : closure S = P
hf : Set.Finite S
⊢ closure ↑(Set.Finite.toFinset hf) = P
[PROOFSTEP]
simp [hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : FG P
S : Set M
hS : closure S = P
hf : Set.Finite S
⊢ AddSubmonoid.closure (↑Additive.toMul ⁻¹' S) = ↑toAddSubmonoid P
[PROOFSTEP]
simp [← Submonoid.toAddSubmonoid_closure, hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : AddSubmonoid.FG (↑toAddSubmonoid P)
T : Set (Additive M)
hT : AddSubmonoid.closure T = ↑toAddSubmonoid P
hf : Set.Finite T
⊢ closure (↑Multiplicative.ofAdd ⁻¹' T) = P
[PROOFSTEP]
simp [← AddSubmonoid.toSubmonoid'_closure, hT]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : AddSubmonoid N
⊢ FG P ↔ Submonoid.FG (↑toSubmonoid P)
[PROOFSTEP]
convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
⊢ FG M
[PROOFSTEP]
cases nonempty_fintype M
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ FG M
[PROOFSTEP]
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤
[PROOFSTEP]
rw [Finset.coe_univ]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure Set.univ = ⊤
[PROOFSTEP]
exact Submonoid.closure_univ
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
[PROOFSTEP]
classical
obtain ⟨s, rfl⟩ := h
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
[PROOFSTEP]
obtain ⟨s, rfl⟩ := h
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ FG (Submonoid.map e (closure ↑s))
[PROOFSTEP]
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (↑e) s) = Submonoid.map e (closure ↑s)
[PROOFSTEP]
rw [Finset.coe_image, MonoidHom.map_mclosure]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
h : FG (Submonoid.map e P)
⊢ FG P
[PROOFSTEP]
obtain ⟨s, hs⟩ := h
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ FG P
[PROOFSTEP]
use s.preimage e (he.injOn _)
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s))) = P
[PROOFSTEP]
apply Submonoid.map_injective_of_injective he
[GOAL]
case h.a
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e (closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s)))) = Submonoid.map e P
[PROOFSTEP]
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
[GOAL]
case h.a
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (↑e '' (↑e ⁻¹' ↑s)) = closure ↑s
[PROOFSTEP]
congr
[GOAL]
case h.a.e_s
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ ↑e '' (↑e ⁻¹' ↑s) = ↑s
[PROOFSTEP]
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs, MonoidHom.mrange_eq_map e]
[GOAL]
case h.a.e_s
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤
[PROOFSTEP]
exact Submonoid.monotone_map le_top
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG N
[PROOFSTEP]
conv_rhs => rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG (Submonoid.map (Submonoid.subtype N) ⊤)
[PROOFSTEP]
exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
[PROOFSTEP]
classical
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
use s.image f
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map, MonoidHom.mrange_top_iff_surjective]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
[PROOFSTEP]
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'
[PROOFSTEP]
use s.image f
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (↑f) s) = ⊤
[PROOFSTEP]
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map, MonoidHom.mrange_top_iff_surjective]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
s : Finset M
⊢ FG { x // x ∈ Submonoid.closure ↑s }
[PROOFSTEP]
refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
s : Finset M
⊢ Submonoid.closure ↑(Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))) = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
x✝ : ∃ S, closure S = P ∧ Set.Finite S
S : Set G
hS : closure S = P
hf : Set.Finite S
⊢ closure ↑(Set.Finite.toFinset hf) = P
[PROOFSTEP]
simp [hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ Submonoid.FG P.toSubmonoid
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P → Submonoid.FG P.toSubmonoid
[PROOFSTEP]
rintro ⟨S, rfl⟩
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.FG (closure ↑S).toSubmonoid
[PROOFSTEP]
rw [Submonoid.fg_iff]
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ Set.Finite S_1
[PROOFSTEP]
refine' ⟨S ∪ S⁻¹, _, S.finite_toSet.union S.finite_toSet.inv⟩
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid
[PROOFSTEP]
exact (Subgroup.closure_toSubmonoid _).symm
[GOAL]
case mpr
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid → FG P
[PROOFSTEP]
rintro ⟨S, hS⟩
[GOAL]
case mpr.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ FG P
[PROOFSTEP]
refine' ⟨S, le_antisymm _ _⟩
[GOAL]
case mpr.intro.refine'_1
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P
[PROOFSTEP]
rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
[GOAL]
case mpr.intro.refine'_1
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
[PROOFSTEP]
exact Submonoid.subset_closure
[GOAL]
case mpr.intro.refine'_2
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
[PROOFSTEP]
rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
[GOAL]
case mpr.intro.refine'_2
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid
[PROOFSTEP]
exact Subgroup.subset_closure
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ AddSubgroup.FG (↑toAddSubgroup P)
[PROOFSTEP]
rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid ↔ AddSubmonoid.FG (↑toAddSubgroup P).toAddSubmonoid
[PROOFSTEP]
exact (Subgroup.toSubmonoid P).fg_iff_add_fg
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : AddSubgroup H
⊢ FG P ↔ Subgroup.FG (↑toSubgroup P)
[PROOFSTEP]
rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : AddSubgroup H
⊢ AddSubmonoid.FG P.toAddSubmonoid ↔ Submonoid.FG (↑toSubgroup P).toSubmonoid
[PROOFSTEP]
exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
⊢ FG G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ FG G
[PROOFSTEP]
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Subgroup.closure_univ⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure ↑Finset.univ = ⊤
[PROOFSTEP]
rw [Finset.coe_univ]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤
[PROOFSTEP]
exact Subgroup.closure_univ
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ FG { x // x ∈ Subgroup.closure ↑s }
[PROOFSTEP]
refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure ↑(Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))) = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage, ← Subgroup.coeSubtype, Subgroup.closure_preimage_eq_top]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ rank G' ≤ rank G
[PROOFSTEP]
classical
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
trans (S.image f).card
· apply Group.rank_le
  rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
· exact Finset.card_image_le.trans_eq hS1
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ rank G' ≤ rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
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
[PROOFSTEP]
trans (S.image f).card
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
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)
[PROOFSTEP]
apply Group.rank_le
[GOAL]
case hS
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
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) = ⊤
[PROOFSTEP]
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
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
[PROOFSTEP]
exact Finset.card_image_le.trans_eq hS1
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup H✝
H K : Subgroup G
inst✝¹ : Group.FG { x // x ∈ H }
inst✝ : Group.FG { x // x ∈ K }
h : H = K
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ K }
[PROOFSTEP]
subst h
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup H✝
H : Subgroup G
inst✝¹ inst✝ : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ H }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
classical
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
  by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)
apply (Group.rank_le (closure (s : Set G)) ht).trans
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
· apply Finset.card_filter_le
· apply Subtype.coe_injective.injOn
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
  by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ closure ↑t = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤
[PROOFSTEP]
exact closure_preimage_eq_top (s : Set G)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
apply (Group.rank_le (closure (s : Set G)) ht).trans
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Finset.card t ≤ Finset.card s
[PROOFSTEP]
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H✝
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ Finset.card t ≤ Finset.card s
case H
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t
[PROOFSTEP]
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H✝
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ Finset.card (Finset.filter (fun x => x ∈ Set.range Subtype.val) s) ≤ Finset.card s
[PROOFSTEP]
apply Finset.card_filter_le
[GOAL]
case H
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t
[PROOFSTEP]
apply Subtype.coe_injective.injOn
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
[PROOFSTEP]
haveI := Fintype.ofFinite s
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
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)
[PROOFSTEP]
exact rank_closure_finset_le_card s.toFinset
