Theorem: Set.ncard_le_fintype_card (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_univ]
State after:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Set.ncard Set.univ

State before:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Set.ncard Set.univ
Tactic:
exact Set.ncard_le_ncard s.subset_univ
State after:
no goals