α : Type u_1
β : Type ?u.18864
γ : Type ?u.18867
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
α : Type u_1
β : Type ?u.18864
γ : Type ?u.18867
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(toOuterMeasure (uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply,Fintype.card_ofFinset]
no goals
α : Type u_1
β : Type ?u.18864
γ : Type ?u.18867
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
rfl