Perfect Secrecy At of uniform Key of unique Key

theorem perfectSecrecyAt_of_uniformKey_of_uniqueKey [LawfulMonad m]    (encAlg : SymmEncAlg m M K C)    [Fintype K]    (deterministicEnc : ∀ (k : K) (msg : M),      ∃ c, support (encAlg.encrypt k msg) = {c}) :    ((∀ k : K, Pr[= k | encAlg.keygen] =        (Fintype.card K : ℝ≥0∞)⁻¹) ∧    (∀ msg : M, ∀ c : C, ∃! k : K,        k ∈ support encAlg.keygen ∧        c ∈ support (encAlg.encrypt k msg))) →    encAlg.perfectSecrecyAt := by  intro ⟨hKeyUniform, hUniqueKey⟩  have hCipherGiven_uniform := encAlg.cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey    deterministicEnc hKeyUniform hUniqueKey  have hCipher_uniform : ∀ (mgen : m M) (σ : C),      Pr[= σ | encAlg.PerfectSecrecyCipherExp mgen] = (Fintype.card K : ℝ≥0∞)⁻¹ := by    intro mgen σ    rw [encAlg.probOutput_PerfectSecrecyCipherExp_eq_tsum mgen σ]    simp_rw [hCipherGiven_uniform _ σ, ENNReal.tsum_mul_right,      tsum_probOutput_of_liftM_PMF mgen, one_mul]  intro mgen msg σ  rw [encAlg.probOutput_PerfectSecrecyExp_eq_mul_cipherGivenMsg mgen msg σ,    hCipherGiven_uniform msg σ, hCipher_uniform mgen σ]