Theorem: Nat.card_subtype (AlgebraI/Subgroups.lean)

State before:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = (Finset.filter p Finset.univ).card
Tactic:
rw [← Fintype.card_subtype]
State after:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = Fintype.card { x // p x }

State before:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = Fintype.card { x // p x }
Tactic:
rw [@card_eq_fintype_card]
State after:
no goals