M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
apply (Group.rank_le (closure (s : Set G)) ht).trans
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H✝ : Type ?u.114818
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.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H✝ : Type ?u.114818
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

case H
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H✝ : Type ?u.114818
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.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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) = ⊤
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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 = ⊤
rw [Finset.coe_preimage]
no goals
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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) = ⊤
exact closure_preimage_eq_top (s : Set G)
no goals
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H✝ : Type ?u.114818
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
apply Finset.card_filter_le
no goals
case H
M : Type ?u.114803
N : Type ?u.114806
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.114818
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
apply Subtype.coe_injective.injOn