awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
false : 1 - (↑p : ℝ≥0∞) = 0 ↔ p = 1
⊢ Bool.false ∈ (bernoulli p h).support ↔
    Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} Bool.false

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]

Premises used: not_iff_not, Bool.cond_prop, ite_false, Bool.false_eq_true, Ne, ENNReal.coe_one, Set.mem_setOf_eq, PMF.mem_support_iff, ENNReal.coe_sub, Bool.cond_false, PMF.bernoulli_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
false : 1 - (↑p : ℝ≥0∞) = 0 → p = 1
false₁ : p = 1 → 1 - (↑p : ℝ≥0∞) = 0
⊢ 1 - (↑p : ℝ≥0∞) = 0 ↔ p = 1

Tactic:
constructor
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
h' : 1 - (↑p : ℝ≥0∞) = 0
⊢ 1 ≤ p

Tactic:
simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'

Premises used: tsub_eq_zero_iff_le, ENNReal.one_le_coe_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
h' : 1 ≤ p
⊢ p = 1

Tactic:
eq_of_le_of_ge h h'

Premises used: eq_of_le_of_ge
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
h' : 1 ≤ p
⊢ p = 1

Tactic:
exact eq_of_le_of_ge h h'

Premises used: eq_of_le_of_ge
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
h' : p = 1
⊢ 1 - (↑p : ℝ≥0∞) = 0

Tactic:
simp only [h', ENNReal.coe_one, tsub_self]

Premises used: tsub_self, ENNReal.coe_one
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} true

Tactic:
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq, ne_eq,
      ENNReal.coe_eq_zero]

Premises used: Bool.cond_true, Set.mem_setOf_eq, ENNReal.coe_eq_zero, ne_eq, PMF.mem_support_iff, PMF.bernoulli_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
rw rw₁ :
  Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
    (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
⊢ 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)

Tactic:
rw [restrict_toMeasure_support p]

Premises used: PMF.restrict_toMeasure_support
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
apply : IntegrableOn (mα := inst) f p.support 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 : α))

Tactic:
apply setIntegral_countable f p.support_countable

Premises used: MeasureTheory.setIntegral_countable, PMF.support_countable
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
rwa : @Integrable _ _ _ _ inst f (Measure.restrict p.toMeasure p.support)
rwa₁ rwa₂ rwa₃ rwa₄ : @Integrable _ _ _ _ inst f p.toMeasure
⊢ IntegrableOn (mα := inst) f p.support p.toMeasure

Tactic:
rwa [IntegrableOn, restrict_toMeasure_support p]

Premises used: MeasureTheory.IntegrableOn, PMF.restrict_toMeasure_support
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
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 : α)
⊢ 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 : α))

Tactic:
congr with x
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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)
e_f :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)} : ℝ≥0∞)
    ((p : (a : α) → ℝ≥0∞) (↑x : α) : ℝ≥0∞)
⊢ ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)}) • f (↑x : α) =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) (↑x : α)) • f (↑x : α)

Tactic:
congr 2
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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)
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {(↑x : α)} : ℝ≥0∞)
    ((p : (a : α) → ℝ≥0∞) (↑x : α) : ℝ≥0∞)

Tactic:
apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Premises used: MeasurableSet.singleton, PMF.toMeasure_apply_singleton, Subtype.val
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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 : α
h1 : Membership.mem (γ := Set α) (Function.support (M := ℝ) fun (a : α) ↦ ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a)) x
h2 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ) ((fun (a : α) ↦ ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a)) x) 0

Tactic:
simp [h2]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
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)
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst p.toMeasure fun (a : α) ↦ f a)
    (∑ a : α, ENNReal.toReal ((p : (a : α) → ℝ≥0∞) a) • f a)

Tactic:
rw [integral_fintype .of_finite]

Premises used: MeasureTheory.integral_fintype, MeasureTheory.Integrable.of_finite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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
e_f : ∀ (x : α), Measure.real (m := inst) p.toMeasure {x} • f x = ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
⊢ 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:
congr with x
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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 : α
e_f :
  ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x}) • f x =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x
⊢ Measure.real (m := inst) p.toMeasure {x} • f x = ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x

Tactic:
rw [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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 : α
e_f : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ ENNReal.toReal (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x}) • f x =
    ENNReal.toReal ((p : (a : α) → ℝ≥0∞) x) • f x

Tactic:
congr 2
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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 : α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Premises used: MeasurableSet.singleton, PMF.toMeasure_apply_singleton
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
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 : α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Premises used: MeasurableSet.singleton, PMF.toMeasure_apply_singleton
-- Module: Mathlib.Probability.ProbabilityMassFunction.Integrals
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ (@integral _ _ _ _ Bool.instMeasurableSpace (bernoulli p h).toMeasure fun (b : Bool) ↦ bif b then 1 else 0) = (↑p : ℝ)

Tactic:
simp [integral_eq_sum]

Premises used: PMF.integral_eq_sum
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a a' : α
⊢ Eq (α := ℝ≥0∞) ((pure a : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (if a' = a then 1 else 0 : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ Membership.mem (γ := Set α) {a} a'

Tactic:
simp [mem_support_iff]

Premises used: PMF.mem_support_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ a' = a

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
⊢ Eq (α := ℝ≥0∞) ((pure a : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a a' : α
h : a' ≠ a
⊢ Eq (α := ℝ≥0∞) ((pure a : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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∞)

Tactic:
(toOuterMeasure_apply (pure a) s).trans ?_

Premises used: PMF.pure, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
refine : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) (if a ∈ s then 1 else 0)
⊢ Eq (α := ℝ≥0∞) (((pure a).toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (if a ∈ s then 1 else 0 : ℝ≥0∞)

Tactic:
refine (toOuterMeasure_apply (pure a) s).trans ?_

Premises used: PMF.pure, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
pos : ∀ (ha : a ∈ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1
neg : ∀ (ha : a ∉ s), Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 0
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) (if a ∈ s then 1 else 0)

Tactic:
split_ifs with ha
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1

Tactic:
(tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)

Premises used: tsum_congr, tsum_ite_eq, OfNat.ofNat, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∈ s
pos : ∀ (b : α), Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) (if b = a then 1 b else 0)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 1

Tactic:
refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)

Premises used: tsum_congr, tsum_ite_eq, OfNat.ofNat, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∈ s
b : α
⊢ Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) (if b = a then 1 b else 0)

Tactic:
ite_eq_left_iff.2 fun hb =>
      symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)

Premises used: Iff.mpr, ite_eq_left_iff, Set.indicator, False.elim, Eq.rec, ite_eq_right_iff, symm, Eq.symm, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∈ s
b : α
⊢ Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) (if b = a then 1 b else 0)

Tactic:
exact ite_eq_left_iff.2 fun hb =>
      symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)

Premises used: Iff.mpr, ite_eq_left_iff, False.elim, ite_eq_right_iff, symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 0

Tactic:
(tsum_congr fun b => ?_).trans tsum_zero

Premises used: tsum_congr, tsum_zero, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∉ s
neg : ∀ (b : α), Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) 0
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) x) 0

Tactic:
refine (tsum_congr fun b => ?_).trans tsum_zero

Premises used: tsum_congr, tsum_zero, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∉ s
b : α
⊢ Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) 0

Tactic:
ite_eq_right_iff.2 fun hb =>
      ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim

Premises used: Iff.mpr, Set.indicator, False.elim, Eq.rec, ite_eq_right_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
ha : a ∉ s
b : α
⊢ Eq (α := ℝ≥0∞) (s.indicator (⇑(pure a) : (a : α) → ℝ≥0∞) b) 0

Tactic:
exact ite_eq_right_iff.2 fun hb =>
      ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
s : Set α
inst : MeasurableSpace α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((pure a).toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (if a ∈ s then 1 else 0 : ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply (pure a) hs).trans (toOuterMeasure_pure_apply a s)

Premises used: PMF.toOuterMeasure_pure_apply, PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.pure, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) (if a ∈ s then 1 else 0) (s.indicator 1 a)
⊢ Eq (α := ℝ≥0∞) ((((pure a).toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]

Premises used: PMF.toMeasure_pure_apply, MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (if a ∈ s then 1 else 0) (s.indicator 1 a)

Tactic:
rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
a : α
inst : MeasurableSpace α
inst_1 : Countable α
h : MeasurableSingletonClass α
rw : Eq (α := Measure α) (Measure.dirac a) (pure a).toMeasure
rw₁ rw₂ : Eq (α := Measure α) (Measure.dirac a) (Measure.dirac a)
⊢ Measure.toPMF (Measure.dirac a) = pure a

Tactic:
rw [toPMF_eq_iff_toMeasure_eq, toMeasure_pure]

Premises used: PMF.toPMF_eq_iff_toMeasure_eq, PMF.toMeasure_pure
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → PMF β
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : α) (a : β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) ((f b : (a : β) → ℝ≥0∞) a : ℝ≥0∞))
    1

Tactic:
simp only [ENNReal.tsum_mul_left, tsum_coe, mul_one]

Premises used: PMF.tsum_coe, ENNReal.tsum_mul_left, mul_one
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ Eq (α := ℝ≥0∞) ((p.bind f : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
rfl

Premises used: tsum, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ Membership.mem (γ := Set β) (⋃ a ∈ p.support, (f a).support) b

Tactic:
simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

Premises used: not_or, PMF.mem_support_iff, ENNReal.tsum_eq_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support

Tactic:
simp only [support_bind, Set.mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, PMF.support_bind, exists_prop
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
h : ∀ (x : β), Eq (α := ℝ≥0∞) (((pure a).bind f : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
⊢ (pure a).bind f = f a

Tactic:
ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
x : β
⊢ Eq (α := ℝ≥0∞) (((pure a).bind f : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) (0 : ℝ≥0∞) = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) y : ℝ≥0∞) ((pure y : (a : α) → ℝ≥0∞) x : ℝ≥0∞) = 0

Tactic:
rw [pure_apply_of_ne _ _ hy.symm, mul_zero]

Premises used: Ne.symm, PMF.pure_apply_of_ne, MulZeroClass.mul_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
p : PMF α
x : α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (1 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) x
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((pure x : (a : α) → ℝ≥0∞) x : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) x

Tactic:
rw [pure_apply_self, mul_one]

Premises used: mul_one, PMF.pure_apply_self
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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
rw₃ rw₄ : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (x : α) ↦ q : PMF β) : (a : β) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]

Premises used: PMF.tsum_coe, ENNReal.tsum_mul_right, PMF.bind_apply, one_mul
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → PMF β
g : β → PMF γ
b : γ
⊢ Eq (α := ℝ≥0∞) (((p.bind f).bind g : (a : γ) → ℝ≥0∞) b : ℝ≥0∞)
    (((p.bind fun (a : α) ↦ (f a).bind g : PMF γ) : (a : γ) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
      ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Premises used: ENNReal.tsum_mul_left, ENNReal.coe_inj, mul_assoc, mul_left_comm, ENNReal.tsum_mul_right, mul_comm, ENNReal.tsum_comm, Eq.symm, PMF.bind_apply, Iff.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : α → β → PMF γ
b : γ
⊢ Eq (α := ℝ≥0∞) (((p.bind fun (a : α) ↦ q.bind (f a) : PMF γ) : (a : γ) → ℝ≥0∞) b : ℝ≥0∞)
    (((q.bind fun (b : β) ↦ p.bind fun (a : α) ↦ f a b : PMF γ) : (a : γ) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
      ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Premises used: ENNReal.tsum_mul_left, ENNReal.coe_inj, mul_assoc, mul_left_comm, ENNReal.tsum_mul_right, mul_comm, ENNReal.tsum_comm, Eq.symm, PMF.bind_apply, Iff.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞) (((p.bind f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (b : β),
        if b ∈ s then
          ∑' (a : α),
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
        else 0 :
      ℝ≥0∞)

Tactic:
simp [toOuterMeasure_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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∞))
neg :
  b ∉ s → Eq (α := ℝ≥0∞) 0 (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥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∞))

Tactic:
split_ifs
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h : 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:
simp