-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem apply_eq_one_iff (p : PMF α) (a : α) : p a = 1 ↔ p.support = {a}

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ (p a + ∑' (b : α), if b = a then 0 else p b) = (if a = a then p a else 0) + ∑' (b : α), if b = a then 0 else p b

Tactic:
rw [eq_self_iff_true, if_true]

Result:
no goals

Proof state:
case e_a
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ (if a = a then p a else 0) = ∑' (b : α), if b = a then p b else 0

Tactic:
exact symm (tsum_eq_single a fun b hb => if_neg hb)

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
b : α
⊢ ((if b = a then p b else 0) + if b = a then 0 else p b) = p b

Tactic:
split_ifs <;> simp only [zero_add, add_zero, le_rfl]

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ 1 < ∑' (a : α), p a

Tactic:
have : 0 < ∑' b, ite (b = a) 0 (p b) := lt_of_le_of_ne' zero_le'
  ((tsum_ne_zero_iff ENNReal.summable).2
    ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)

Result:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ 1 < ∑' (a : α), p a

Proof state:
α : Type u_1
p : PMF α
a : α
⊢ p a = 1 ↔ p.support = {a}

Tactic:
refine ⟨fun h => Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_)
  fun a' ha' => ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
  fun h => _root_.trans (symm <| tsum_eq_single a
    fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩

Result:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ False

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ ((if a = a then p a else 0) + ∑' (b : α), if b = a then 0 else p b) =
    (∑' (b : α), if b = a then p b else 0) + ∑' (b : α), if b = a then 0 else p b

Tactic:
congr

Result:
case e_a
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ (if a = a then p a else 0) = ∑' (b : α), if b = a then p b else 0

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ 1 < ∑' (a : α), p a

Tactic:
calc
  1 = 1 + 0 := (add_zero 1).symm
  _ < p a + ∑' b, ite (b = a) 0 (p b) :=
    (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
  _ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
  _ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) := by
    congr
    exact symm (tsum_eq_single a fun b hb => if_neg hb)
  _ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
  _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero, le_rfl]

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ False

Tactic:
suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm

Result:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ 1 < ∑' (a : α), p a

Proof state:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ 1 < ∑' (a : α), p a

Tactic:
classical
have : 0 < ∑' b, ite (b = a) 0 (p b) := lt_of_le_of_ne' zero_le'
  ((tsum_ne_zero_iff ENNReal.summable).2
    ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
calc
  1 = 1 + 0 := (add_zero 1).symm
  _ < p a + ∑' b, ite (b = a) 0 (p b) :=
    (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
  _ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
  _ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) := by
    congr
    exact symm (tsum_eq_single a fun b hb => if_neg hb)
  _ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
  _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero, le_rfl]

Result:
no goals