Constant of exists one

theorem constant_of_exists_one {D : ProbDistribution α} {x : α} (h : D x = 1) : D = ProbDistribution.constant x := by  ext y  by_cases h₂ : x = y  · simp [h, ← h₂]  · simp only [constant_eq, h₂, ↓reduceIte, Prob.coe_zero]    by_contra h₃    replace h₃ : 0 < (D y : ℝ) := by      linarith (config := {splitNe := true}) only [h₃, @Prob.zero_le_coe (D y)]    have := D.normalized    rw [← Finset.add_sum_erase _ _ (Finset.mem_univ x), h, Prob.coe_one] at this    rw [← Finset.add_sum_erase _ _ (a := y) (by simpa using (Ne.symm h₂))] at this    have : 0 ≤ ∑ x ∈ Finset.erase (Finset.erase Finset.univ x) y, (D x : ℝ) :=      Finset.sum_nonneg' (fun _ ↦ Prob.zero_le_coe)    linarith