-- Mathlib/GroupTheory/Finiteness.lean
theorem rank_closure_finset_le_card (s : Finset G) : Group.rank (closure (s : Set G)) ≤ s.card

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Tactic:
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Tactic:
have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t

Tactic:
apply Subtype.coe_injective.injOn

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤

Tactic:
exact closure_preimage_eq_top (s : Set G)

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Tactic:
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))) by
  rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
  apply Finset.card_filter_le
apply Subtype.coe_injective.injOn

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure ↑t = ⊤

Tactic:
rw [Finset.coe_preimage]

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ t.card ≤ s.card

Tactic:
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
  rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
  apply Finset.card_filter_le

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ (Finset.filter (fun x => x ∈ Set.range Subtype.val) s).card ≤ s.card

Tactic:
apply Finset.card_filter_le

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ t.card ≤ s.card

Tactic:
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ (Finset.filter (fun x => x ∈ Set.range Subtype.val) s).card ≤ s.card

Proof state:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Group.rank ↥(closure ↑s) ≤ s.card

Tactic:
apply (Group.rank_le (closure (s : Set G)) ht).trans

Result:
G : Type u_3
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ t.card ≤ s.card