awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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)
rw :
  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 True then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
⊢ 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∞)
have rw₁ : 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∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: rw [eq_self_iff_true, if_true]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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∞) (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)
have e_a : Eq (α := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
  (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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)
b : α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
      (if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) b
have pos : b = a → HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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)
b : α
pos : b = a → HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
      (if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) b
have neg : ¬b = a → HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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)
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have _ : 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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∞)
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have _₁ : 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)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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}
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have have : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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)
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
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)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
have refine : ∀ (b : α), LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a b : α
⊢ LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
have pos : ∀ (h : b = a), LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
have neg : ∀ (h : ¬b = a), LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
⊢ LE.le (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
have refine : ∀ (b : α), LE.le (α := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: classical
  refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
  split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
⊢ p.toOuterMeasure.caratheodory = ⊤
have 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
Tactic: refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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
⊢ ⊤ ≤ x
have have : ∀ (y : α) (hy : (fun (i : α) ↦ (HSMul.hSMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (dirac i)).caratheodory) y = x),
  ⊤ ≤ x
Tactic: have ⟨y, hy⟩ := hx
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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∞)
have refine_1 : ∀ b ∉ s, Eq (α := ℝ≥0∞) ((↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) 0
Tactic: refine (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
s : Finset α
refine_1 : ∀ b ∉ s, Eq (α := ℝ≥0∞) ((↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) 0
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) (∑ b ∈ s, (↑s : Set α).indicator (⇑p : (a : α) → ℝ≥0∞) b) (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x)
Tactic: refine (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
have refine_1 : ∀ (b : α) (hb : b ≠ a), Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0
Tactic: refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
refine_1 : ∀ (b : α) (hb : b ≠ a), Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) b) 0
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) (Set.indicator {a} (⇑p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s
have rw : (∀ (i : α), Eq (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) i) 0) ↔ Disjoint p.support s
Tactic: rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support ⊆ s
have refine_1 : ∀ (h : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1) (a : α) (hap : a ∈ p.support), a ∈ s
Tactic: refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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
⊢ Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support ⊆ s
have refine_2 : ∀ (h : p.support ⊆ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
Tactic: refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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
have refine_1 : ∀ (hs : a ∉ s), LT.lt (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
Tactic: refine by_contra fun hs => ne_of_lt ?_ (h.trans p.tsum_coe.symm)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (hypothesis)
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
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have hs' : 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'
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (hypothesis)
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∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have hsa : 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
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
have refine_2 : ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x) 1
have refine_2 : ∀ x ∉ s, Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s
have rw : Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s
Tactic: rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Disjoint p.support s
have rw₁ : Disjoint p.support s ↔ Disjoint p.support s
Tactic: rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
h : s ∩ p.support ⊆ t
⊢ LE.le (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
⊢ Eq (α := Measure α) (Measure.restrict p.toMeasure p.support) p.toMeasure
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply hs, p.toMeasure_apply_inter_support hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply hs, p.toMeasure_apply_inter_support hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
h : Eq (α := Measure α) p.toMeasure q.toMeasure
⊢ p = q
have h₁ : ∀ (x : α), Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
h : Eq (α := Measure α) p.toMeasure q.toMeasure
x : α
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
    ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
h : Eq (α := Measure α) p.toMeasure q.toMeasure
x : α
h₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
  (((q.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
Tactic: rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
    ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
h : Eq (α := Measure α) p.toMeasure q.toMeasure
x : α
h₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((q.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) (((q.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
  (((q.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
Tactic: rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
    ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have hs : MeasurableSet (s ∩ p.support)
Tactic: have hs := (p.support_countable.mono s.inter_subset_right).measurableSet
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet (s ∩ p.support)
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← restrict_toMeasure_support, Measure.restrict_apply' p.support_countable.measurableSet,
    p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_inter_support]