Ciphertext Indist of perfectly Secret

theorem ciphertextIndist_of_perfectlySecret (scheme : EncScheme M K C)    (h : scheme.PerfectlySecret) :    scheme.CiphertextIndist := by  classical  rw [perfectlySecret_iff_indep] at h  intro m₀ m₁; ext c  have hs : ({m₀, m₁} : Finset M).Nonempty := ⟨m₀, Finset.mem_insert_self ..⟩  set μ := PMF.uniformOfFinset _ hs  suffices key : ∀ m ∈ ({m₀, m₁} : Finset M),      scheme.ciphertextDist m c = scheme.marginalCiphertextDist μ c by    exact (key m₀ (by simp)).trans (key m₁ (by simp)).symm  intro m hm  have hne := (PMF.mem_support_uniformOfFinset_iff hs m).mpr hm  have hne_top := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ m)  exact (ENNReal.mul_right_inj hne hne_top).mp (by rw [← jointDist_eq]; exact h μ m c)