awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
rw :
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) 0 (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
Tactic: rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
rw :
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
rw₁ : HMul.hMul (α := ℝ≥0∞) 0 (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s ∨ a ∉ p.support
have rw : a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
Tactic: rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s ∨ a ∉ p.support
have rw₁ : a ∉ s ∩ p.support ↔ a ∉ s ∨ a ∉ p.support
Tactic: rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
rw₁ : a ∉ s ∩ p.support ↔ a ∉ s ∨ a ∉ p.support
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s ∨ a ∉ p.support
have rw₂ : ¬(a ∈ s ∧ a ∈ p.support) ↔ a ∉ s ∨ a ∉ p.support
Tactic: rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
rw₁ : a ∉ s ∩ p.support ↔ a ∉ s ∨ a ∉ p.support
rw₂ : ¬(a ∈ s ∧ a ∈ p.support) ↔ a ∉ s ∨ a ∉ p.support
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s ∨ a ∉ p.support
have rw₃ : a ∉ s ∨ a ∉ p.support ↔ a ∉ s ∨ a ∉ p.support
Tactic: rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
have rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
Tactic: rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
have rw₁ : ¬(a ∉ s ∨ a ∉ p.support) ↔ a ∈ s ∧ a ∈ p.support
Tactic: rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
rw₁ : ¬(a ∉ s ∨ a ∉ p.support) ↔ a ∈ s ∧ a ∈ p.support
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
have rw₂ : ¬a ∉ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
Tactic: rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
rw₁ : ¬(a ∉ s ∨ a ∉ p.support) ↔ a ∈ s ∧ a ∈ p.support
rw₂ : ¬a ∉ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
have rw₃ : a ∈ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
Tactic: rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
rw₁ : ¬(a ∉ s ∨ a ∉ p.support) ↔ a ∈ s ∧ a ∈ p.support
rw₂ : ¬a ∉ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
rw₃ : a ∈ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
have rw₄ : a ∈ s ∧ a ∈ p.support ↔ a ∈ s ∧ a ∈ p.support
Tactic: rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bernoulli p h : (a : Bool) → ℝ≥0∞) b = (↑(bif b then p else 1 - p) : ℝ≥0∞)
have simp : (bif b then (↑p : ℝ≥0∞) else 1 - (↑p : ℝ≥0∞)) = (↑(bif b then p else 1 - p) : ℝ≥0∞)
Tactic: simp only [bernoulli, ofFintype_apply]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ (bernoulli p h).support = {b : Bool | bif b then p ≠ 0 else p ≠ 1}
have refine : ∀ (b : Bool), b ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} b
Tactic: refine Set.ext fun b => ?_
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} b
have false : false ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} false
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
false :
  Bool.false ∈ (bernoulli p h).support ↔
    Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} Bool.false
⊢ b ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} b
have true : true ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} true
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} false
have false : 1 - (↑p : ℝ≥0∞) = 0 ↔ p = 1
Tactic: simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne, ENNReal.coe_sub,
      ENNReal.coe_one, Bool.cond_prop, Set.mem_setOf_eq, Bool.false_eq_true, ite_false, not_iff_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ 1 - (↑p : ℝ≥0∞) = 0 ↔ p = 1
have false : 1 - (↑p : ℝ≥0∞) = 0 → p = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
false : 1 - (↑p : ℝ≥0∞) = 0 → p = 1
⊢ 1 - (↑p : ℝ≥0∞) = 0 ↔ p = 1
have false₁ : p = 1 → 1 - (↑p : ℝ≥0∞) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (hypothesis)
Goal:
p : ℝ≥0
h : p ≤ 1
h' : 1 - (↑p : ℝ≥0∞) = 0
⊢ p = 1
have h'₁ : 1 ≤ p
Tactic: simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
p : PMF α
f : α → E
hf : @Integrable _ _ _ _ inst f p.toMeasure
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
    (@integral _ _ _ _ inst (Measure.restrict p.toMeasure p.support) fun (a : α) ↦ f a)
have rw : Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
  (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
Tactic: rw [restrict_toMeasure_support p]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
p : PMF α
f : α → E
hf : @Integrable _ _ _ _ inst f p.toMeasure
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst (Measure.restrict p.toMeasure p.support) fun (a : α) ↦ f a)
    (∑' (a : (↑p.support : Type u_1)),
      ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑a : α)}) • f (↑a : α))
have apply : IntegrableOn (mα := inst) f p.support p.toMeasure
Tactic: apply setIntegral_countable f p.support_countable
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
p : PMF α
f : α → E
hf : @Integrable _ _ _ _ inst f p.toMeasure
⊢ IntegrableOn (mα := inst) f p.support p.toMeasure
have rwa : @Integrable _ _ _ _ inst f (Measure.restrict p.toMeasure p.support)
Tactic: rwa [IntegrableOn, restrict_toMeasure_support p]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
p : PMF α
f : α → E
hf : @Integrable _ _ _ _ inst f p.toMeasure
⊢ Eq.{u_2 + 1} (α := E)
    (∑' (a : (↑p.support : Type u_1)),
      ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑a : α)}) • f (↑a : α))
    (∑' (a : (↑p.support : Type u_1)), ENNReal.toReal ((p : (a : α) → ℝ≥0∞) (↑a : α)) • f (↑a : α))
have e_f : ∀ (x : (↑p.support : Type u_1)),
  ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)}) • f (↑x : α) =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) (↑x : α)) • f (↑x : α)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
p : PMF α
f : α → E
hf : @Integrable _ _ _ _ inst f p.toMeasure
x : (↑p.support : Type u_1)
⊢ ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)}) • f (↑x : α) =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) (↑x : α)) • f (↑x : α)
have e_f : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)} : ℝ≥0∞)
  ((p : (a : α) → ℝ≥0∞) (↑x : α) : ℝ≥0∞)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : Fintype α
p : PMF α
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
    (∑ a : α, ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a) • f a)
have rw : Eq.{u_2 + 1} (α := E) (∑ x : α, Measure.real (m := inst) p.toMeasure {x} • f x)
  (∑ a : α, ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a) • f a)
Tactic: rw [integral_fintype .of_finite]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : Fintype α
p : PMF α
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (∑ x : α, Measure.real (m := inst) p.toMeasure {x} • f x)
    (∑ a : α, ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a) • f a)
have e_f : ∀ (x : α), Measure.real (m := inst) p.toMeasure {x} • f x = ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : Fintype α
p : PMF α
f : α → E
x : α
⊢ Measure.real (m := inst) p.toMeasure {x} • f x = ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
have e_f : ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x}) • f x =
  ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
Tactic: rw [measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Integrals (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : Fintype α
p : PMF α
f : α → E
x : α
⊢ ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x}) • f x =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
have e_f : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((pure a).toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (if a ∈ s then 1 else 0 : ℝ≥0∞)
have refine : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) (if a ∈ s then 1 else 0)
Tactic: refine (toOuterMeasure_apply (pure a) s).trans ?_
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
s : Set α
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) (if a ∈ s then 1 else 0)
have pos : ∀ (ha : a ∈ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
s : Set α
pos : ∀ (ha : a ∈ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) (if a ∈ s then 1 else 0)
have neg : ∀ (ha : a ∉ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 0
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1
have pos : ∀ (b : α), Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) (if b = a then 1 b else 0)
Tactic: refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 0
have neg : ∀ (b : α), Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) 0
Tactic: refine (tsum_congr fun b => ?_).trans tsum_zero
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((pure a).toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (if a ∈ s then 1 else 0) (s.indicator 1 a)
Tactic: rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
inst_1 : Countable α
h : MeasurableSingletonClass α
⊢ Measure.toPMF (Measure.dirac a) = pure a
have rw : Eq (α := Measure α) (Measure.dirac a) (pure a).toMeasure
Tactic: rw [toPMF_eq_iff_toMeasure_eq, toMeasure_pure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
inst_1 : Countable α
h : MeasurableSingletonClass α
rw : Eq (α := Measure α) (Measure.dirac a) (pure a).toMeasure
⊢ Measure.toPMF (Measure.dirac a) = pure a
have rw₁ : Eq (α := Measure α) (Measure.dirac a) (Measure.dirac a)
Tactic: rw [toPMF_eq_iff_toMeasure_eq, toMeasure_pure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
⊢ (pure a).bind f = f a
have h : ∀ (x : β), Eq (α := ℝ≥0∞) (((pure a).bind f : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) ((pure y : (a : α) → ℝ≥0∞) x : ℝ≥0∞) = 0
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) (0 : ℝ≥0∞) = 0
Tactic: rw [pure_apply_of_ne _ _ hy.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) (0 : ℝ≥0∞) = 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) ((pure y : (a : α) → ℝ≥0∞) x : ℝ≥0∞) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [pure_apply_of_ne _ _ hy.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
p : PMF α
x : α
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((pure x : (a : α) → ℝ≥0∞) x : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) x
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (1 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) x
Tactic: rw [pure_apply_self, mul_one]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
p : PMF α
x : α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (1 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) x
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((pure x : (a : α) → ℝ≥0∞) x : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) x
have rw₁ : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: rw [pure_apply_self, mul_one]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (x : α) ↦ q : PMF β) : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) : ℝ≥0∞)
  ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
rw :
  Eq (α := ℝ≥0∞)
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) :
      ℝ≥0∞)
    ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (x : α) ↦ q : PMF β) : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : α), (p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) =
  (q : (a : β) → ℝ≥0∞) x
Tactic: rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
rw :
  Eq (α := ℝ≥0∞)
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) :
      ℝ≥0∞)
    ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : α), (p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) =
    (q : (a : β) → ℝ≥0∞) x
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (x : α) ↦ q : PMF β) : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
have rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) = (q : (a : β) → ℝ≥0∞) x
Tactic: rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
rw :
  Eq (α := ℝ≥0∞)
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) :
      ℝ≥0∞)
    ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : α), (p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) =
    (q : (a : β) → ℝ≥0∞) x
rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) = (q : (a : β) → ℝ≥0∞) x
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (x : α) ↦ q : PMF β) : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
⊢ Eq (α := ℝ≥0∞)
    (if b ∈ s then
      ∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    else 0)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))
have pos : b ∈ s →
  Eq (α := ℝ≥0∞)
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
pos :
  b ∈ s →
    Eq (α := ℝ≥0∞)
      (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
      (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞)
    (if b ∈ s then
      ∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    else 0)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))
have neg : b ∉ s → Eq (α := ℝ≥0∞) 0 (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
⊢ Eq (α := ℝ≥0∞) (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)
    (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)
have pos : b ∈ s → Eq (α := ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: split_ifs