α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ False
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
⊢ ↑p a = 1 ↔ support p = {a}
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⟩
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 1 < ∑' (a : α), ↑p a
⊢ False

case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ False
suffices : 1 < ∑' a, p a
case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 1 < ∑' (a : α), ↑p a
⊢ False

case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
exact ne_of_lt this p.tsum_coe.symm
case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ 1 < ∑' (a : α), ↑p a
case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
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'⟩⟩)
no goals
case this
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ 1 < ∑' (a : α), ↑p a
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]
no goals
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
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
rw [eq_self_iff_true, if_true]
case e_a
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
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
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
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
congr
no goals
case e_a
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
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
exact symm (tsum_eq_single a fun b hb => if_neg hb)
no goals
α : Type u_1
β : Type ?u.6948
γ : Type ?u.6951
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
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
split_ifs <;> simp only [zero_add, add_zero, le_rfl]