α : Type u_1
β : Type ?u.17026
γ : Type ?u.17029
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ Finset.card Finset.univ = Fintype.card α
α : Type u_1
β : Type ?u.17026
γ : Type ?u.17029
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ ↑(uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
simp [uniformOfFintype, Finset.mem_univ, if_true, uniformOfFinset_apply]
no goals
α : Type u_1
β : Type ?u.17026
γ : Type ?u.17029
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ Finset.card Finset.univ = Fintype.card α
rfl