awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
_ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
_₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) 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]

Premises used: ENNReal.add_lt_add_of_le_of_lt, ENNReal.tsum_add, tsum_congr, tsum, le_of_eq, add_zero, OfNat.ofNat, Eq.symm, Eq, DFunLike.coe, SummationFilter.unconditional, ENNReal.one_ne_top, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
have : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
have₁ :
  ∀ (this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)),
    LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have₂ : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
have₃ have₄ :
  ∀ (this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)),
    LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)

Tactic:
classical
  have : 0 < ∑' b, ite (b = a) 0 (p b) := by
    rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]
    exact ⟨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]

Premises used: ENNReal.tsum_add, tsum_congr, add_zero, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)

Premises used: hasSum_le, hasSum_ite_eq, PMF.hasSum_coe_one, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
refine :
  ∀ (b : α), LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)

Premises used: hasSum_le, hasSum_ite_eq, PMF.hasSum_coe_one, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
pos : ∀ (h : b = a), LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
neg : ∀ (h : ¬b = a), LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
h : b = a
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
h : ¬b = a
⊢ LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
refine :
  ∀ (b : α), LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
classical
  refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
  split_ifs with h <;> simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt (lt_of_le_of_lt (p.coe_le_one a) ENNReal.one_lt_top)

Premises used: lt_of_le_of_lt, ENNReal.one_lt_top, PMF.coe_le_one, ne_of_lt
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ LT.lt (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_ne le_top (p.apply_ne_top a)

Premises used: le_top, PMF.apply_ne_top, lt_of_le_of_ne
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
tsum_congr fun x => smul_dirac_apply (p x) x s

Premises used: tsum_congr, tsum, MeasureTheory.OuterMeasure.smul_dirac_apply, DFunLike.coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ p.toOuterMeasure.caratheodory = ⊤

Tactic:
eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)

Premises used: Iff.mpr, eq_top_iff, MeasureTheory.OuterMeasure.le_sum_caratheodory, le_sInf, le_trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
refine :
  ∀ (x : MeasurableSpace α)
    (hx :
      Membership.mem (γ := Set (MeasurableSpace α))
        (Set.range fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) x),
    ⊤ ≤ x
⊢ p.toOuterMeasure.caratheodory = ⊤

Tactic:
refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)

Premises used: Iff.mpr, eq_top_iff, MeasureTheory.OuterMeasure.le_sum_caratheodory, le_sInf, le_trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx :
  Membership.mem (γ := Set (MeasurableSpace α))
    (Set.range fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) x
have :
  ∀ (y : α)
    (hy : (fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) y = x), ⊤ ≤ x
⊢ ⊤ ≤ x

Tactic:
have ⟨y, hy⟩ := hx
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx :
  Membership.mem (γ := Set (MeasurableSpace α))
    (Set.range fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) x
y : α
hy : (fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) y = x
⊢ ⊤ ≤ x

Tactic:
((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

Premises used: MeasureTheory.OuterMeasure.le_smul_caratheodory, LE.le.trans, le_of_eq, MeasureTheory.OuterMeasure.dirac_caratheodory, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx :
  Membership.mem (γ := Set (MeasurableSpace α))
    (Set.range fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) x
y : α
hy : (fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) y = x
⊢ ⊤ ≤ x

Tactic:
exact
    ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

Premises used: MeasureTheory.OuterMeasure.le_smul_caratheodory, LE.le.trans, le_of_eq, MeasureTheory.OuterMeasure.dirac_caratheodory, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)

Premises used: SetLike.coe, tsum_eq_sum, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
refine_1 : ∀ b ∉ s, Eq (α := ℝ≥0∞) ((↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) 0
refine_2 : Eq (α := ℝ≥0∞) (∑ b ∈ s, (↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x)
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
refine (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)

Premises used: SetLike.coe, tsum_eq_sum, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, Eq (α := ℝ≥0∞) ((↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) 0

Tactic:
fun x hx => Set.indicator_of_notMem (Finset.mem_coe.not.2 hx) _

Premises used: Iff.mpr, Iff.not, Set.indicator_of_notMem, DFunLike.coe, Finset.mem_coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, Eq (α := ℝ≥0∞) ((↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) 0

Tactic:
exact fun x hx => Set.indicator_of_notMem (Finset.mem_coe.not.2 hx) _

Premises used: Iff.mpr, Iff.not, Set.indicator_of_notMem, Finset.mem_coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
⊢ Eq (α := ℝ≥0∞) (∑ b ∈ s, (↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x)

Tactic:
Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _

Premises used: Iff.mpr, Set.indicator_of_mem, DFunLike.coe, Finset.mem_coe, Finset.sum_congr, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Finset α
⊢ Eq (α := ℝ≥0∞) (∑ b ∈ s, (↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x)

Tactic:
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _

Premises used: Iff.mpr, Set.indicator_of_mem, Finset.mem_coe, Finset.sum_congr, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
(p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)

Premises used: tsum_eq_single, PMF.toOuterMeasure_apply, Singleton.singleton, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
refine_1 : ∀ (b : α) (hb : b ≠ a), Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0
refine_2 : Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)

Premises used: tsum_eq_single, PMF.toOuterMeasure_apply, Singleton.singleton, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0

Tactic:
ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Premises used: Iff.mpr, Set.indicator, False.elim, ite_eq_right_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0

Tactic:
exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Premises used: Iff.mpr, False.elim, ite_eq_right_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0

Tactic:
classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Premises used: Iff.mpr, False.elim, ite_eq_right_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Premises used: Iff.mpr, ite_eq_left_iff, Set.indicator, False.elim, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Premises used: Iff.mpr, ite_eq_left_iff, False.elim, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
classical exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Premises used: Iff.mpr, ite_eq_left_iff, False.elim, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := PMF α) toOuterMeasure

Tactic:
fun p q h => PMF.ext fun x => (p.toOuterMeasure_apply_singleton x).symm.trans
    ((congr_fun (congr_arg _ h) _).trans <| q.toOuterMeasure_apply_singleton x)

Premises used: PMF.toOuterMeasure_apply_singleton, congr_arg, PMF.ext, Function.Injective, congr_fun, Singleton.singleton, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p q : PMF α
⊢ p.toOuterMeasure = q.toOuterMeasure ↔ p = q

Tactic:
toOuterMeasure_injective.eq_iff

Premises used: PMF.toOuterMeasure_injective, Function.Injective.eq_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
rw : (∀ (i : α), Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) i) 0) ↔ Disjoint p.support s
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s

Tactic:
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]

Premises used: PMF.toOuterMeasure_apply, ENNReal.tsum_eq_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) i) 0) ↔ Disjoint p.support s

Tactic:
funext_iff.symm.trans Set.indicator_eq_zero'

Premises used: funext_iff, Set.indicator_eq_zero', Iff.trans, Iff.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) i) 0) ↔ Disjoint p.support s

Tactic:
exact funext_iff.symm.trans Set.indicator_eq_zero'

Premises used: funext_iff, Set.indicator_eq_zero', Iff.trans, Iff.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support ⊆ s

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

Premises used: Eq.rec, Iff.intro, PMF.toOuterMeasure_apply, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
refine_1 :
  ∀ (h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1) (a : α) (hap : a ∈ p.support), a ∈ s
refine_2 : ∀ (h : p.support ⊆ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support ⊆ s

Tactic:
refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
⊢ a ∈ s

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

Premises used: PMF.tsum_coe, by_contra, Eq.symm, ne_of_lt, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
refine_1 :
  ∀ (hs : a ∉ s),
    LT.lt (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
⊢ a ∈ s

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

Premises used: PMF.tsum_coe, by_contra, Eq.symm, ne_of_lt, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
hs : a ∉ s
⊢ Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) 0

Tactic:
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) 0
⊢ LT.lt (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) 0
hsa : LT.lt (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)

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

Premises used: le_rfl, ENNReal.tsum_lt_tsum, PMF.tsum_coe_indicator_ne_top, Set.indicator_apply_le
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
a : α
hap : a ∈ p.support
hs : a ∉ s
hs' : Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) 0
hsa : LT.lt (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)

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

Premises used: le_rfl, ENNReal.tsum_lt_tsum, PMF.tsum_coe_indicator_ne_top, Set.indicator_apply_le
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
refine_2 : ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) 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
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
refine_2 : ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) 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
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, PMF.apply_eq_zero_iff, Set.notMem_subset
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, PMF.apply_eq_zero_iff, Set.notMem_subset
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [toOuterMeasure_apply, PMF.support, Set.indicator_inter_support]

Premises used: Set.indicator_inter_support, PMF.support, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s t : Set α
h : s ∩ p.support ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_trans (le_of_eq (toOuterMeasure_apply_inter_support p s).symm) (p.toOuterMeasure.mono h)

Premises used: MeasureTheory.OuterMeasure.mono, PMF.toOuterMeasure, PMF.toOuterMeasure_apply_inter_support, le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s t : Set α
h : s ∩ p.support = t ∩ p.support
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_antisymm (p.toOuterMeasure_mono (h.symm ▸ Set.inter_subset_left))
    (p.toOuterMeasure_mono (h ▸ Set.inter_subset_left))

Premises used: PMF.toOuterMeasure_mono, Eq.rec, Set.inter_subset_left, le_antisymm, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
inst : Fintype α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ x : α, s.indicator (⇑p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(p.toOuterMeasure_apply s).trans (tsum_eq_sum fun x h => absurd (Finset.mem_univ x) h)

Premises used: Finset.mem_univ, absurd, tsum_eq_sum, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_toMeasure_apply p.toOuterMeasure _ s

Premises used: PMF.toOuterMeasure, MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
toMeasure_apply p.toOuterMeasure _ hs

Premises used: PMF.toOuterMeasure, MeasureTheory.toMeasure_apply