ProbabilityTheory.entropy_of_uniformOn

lemma entropy_of_uniformOn (H : Set S) [Nonempty H] [Finite H] :    measureEntropy (uniformOn H) = log (Nat.card H) := by  simp only [measureEntropy, measure_univ, inv_one, one_smul, Set.toFinite, uniformOn_real]  classical  calc ∑' s, negMulLog ((Nat.card (H ∩ {s} : Set S)) / Nat.card H)    _ = ∑' s, if s ∈ H then negMulLog (1 / Nat.card H) else 0 := by      congr with s; by_cases h : s ∈ H <;> simp [h]    _ = ∑ s ∈ H.toFinite.toFinset, negMulLog (1 / Nat.card H) := by      convert tsum_eq_sum (s := H.toFinite.toFinset) ?_ using 2 with s hs      · simp at hs; simp [hs]      · constructor        simp      intro s hs      simp only [Set.Finite.mem_toFinset] at hs; simp [hs]    _ = (Nat.card H) * negMulLog (1 / Nat.card H) := by simp [← Set.ncard_coe_finset]    _ = log (Nat.card H) := by      simp only [negMulLog, one_div, log_inv, mul_neg, neg_mul, neg_neg, ← mul_assoc]      rw [mul_inv_cancel₀, one_mul]      simp only [ne_eq, Nat.cast_eq_zero, Nat.card_ne_zero]      exact ⟨‹_›, ‹_›⟩