Theorem: Finset.card_mulStab_le_card (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab.card ≤ s.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab.card ≤ ∅.card

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab.card ≤ s.card

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab.card ≤ ∅.card
Tactic:
rfl
State after:
no goals

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab.card ≤ s.card
Tactic:
exact Nat.le_of_dvd hs.card_pos s.card_mulStab_dvd_card
State after:
no goals