Theorem: Equiv.encard_univ_eq (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α ≃ β
⊢ univ.encard = univ.encard
Tactic:
rw [encard_univ, encard_univ, PartENat.card_congr e]
State after:
no goals