Cipher Given Msg uniform of uniform Key of unique Key

theorem cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey    (encAlg : SymmEncAlg m M K C) [Fintype K]    (deterministicEnc : ∀ (k : K) (msg : M),      ∃ c, support (encAlg.encrypt k msg) = {c})    (hKeyUniform : ∀ k : K, Pr[= k | encAlg.keygen] =        (Fintype.card K : ℝ≥0∞)⁻¹)    (hUniqueKey : ∀ msg : M, ∀ c : C, ∃! k : K,        k ∈ support encAlg.keygen ∧        c ∈ support (encAlg.encrypt k msg))    (msg : M) (σ : C) :    Pr[= σ | encAlg.PerfectSecrecyCipherGivenMsgExp msg] =      (Fintype.card K : ℝ≥0∞)⁻¹ := by  obtain ⟨k0, hk0, hk0uniq⟩ := hUniqueKey msg σ  have henc_one : Pr[= σ | encAlg.encrypt k0 msg] = 1 := by    obtain ⟨c0, hc0⟩ := deterministicEnc k0 msg    obtain rfl : σ = c0 := by simpa [hc0] using hk0.2    exact probOutput_eq_one_iff.2 ⟨probFailure_of_liftM_PMF _, by simpa using hc0⟩  simp only [PerfectSecrecyCipherGivenMsgExp, probOutput_bind_eq_tsum]  rw [tsum_eq_single k0 fun k hkne => mul_eq_zero.2 <|    (not_and_or.1 fun h => hkne (hk0uniq k h)).imp      probOutput_eq_zero_of_not_mem_support probOutput_eq_zero_of_not_mem_support]  simp [hKeyUniform k0, henc_one]