-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_apply_eq_one_iff : p.toOuterMeasure s = 1 ↔ p.support ⊆ s

Proof state:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0

Tactic:
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.not_mem_subset h ha

Result:
no goals

Proof state:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : s.indicator (⇑p) a = 0
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Tactic:
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap

Result:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : s.indicator (⇑p) a = 0
hsa : s.indicator (⇑p) a < p a
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Proof state:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
⊢ a ∈ s

Tactic:
refine by_contra fun hs => ne_of_lt ?_ (h.trans p.tsum_coe.symm)

Result:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Proof state:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
classical suffices ∀ (x) (_ : x ∉ s), p x = 0 from
  _root_.trans (tsum_congr
    fun a => (Set.indicator_apply s p a).trans
      (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe

Result:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0

Proof state:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : s.indicator (⇑p) a = 0
hsa : s.indicator (⇑p) a < p a
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Tactic:
exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s)
  (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa

Result:
no goals

Proof state:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Tactic:
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'

Result:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : s.indicator (⇑p) a = 0
⊢ ∑' (x : α), s.indicator (⇑p) x < ∑' (a : α), p a

Proof state:
α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure s = 1 ↔ p.support ⊆ s

Tactic:
refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
⊢ a ∈ s

case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Proof state:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
suffices ∀ (x) (_ : x ∉ s), p x = 0 from
_root_.trans (tsum_congr
fun a => (Set.indicator_apply s p a).trans
(ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe

Result:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0