awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
    (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(p.toMeasure_apply_eq_toOuterMeasure_apply hs).trans (p.toOuterMeasure_apply s)

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
a : α
h : MeasurableSet (α := α) {a}
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
simp [p.toMeasure_apply_eq_toOuterMeasure_apply h, toOuterMeasure_apply_singleton]

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_apply_singleton
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
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
rw₁ rw₂ : Disjoint p.support s ↔ Disjoint p.support s
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (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]

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_apply_eq_zero_iff
-- 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∞) (1 : ℝ≥0∞) ↔ p.support ⊆ s

Tactic:
(p.toMeasure_apply_eq_toOuterMeasure_apply hs).symm ▸ p.toOuterMeasure_apply_eq_one_iff s

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, Eq.rec, Eq.symm, PMF.toOuterMeasure_apply_eq_one_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
h : s ∩ p.support ⊆ t
rw :
  LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs]

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
h : s ∩ p.support ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(p.toOuterMeasure_mono h).trans (p.toOuterMeasure_apply_le_toMeasure_apply t)

Premises used: PMF.toOuterMeasure_mono, PMF.toOuterMeasure_apply_le_toMeasure_apply, LE.le.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
h : s ∩ p.support ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact (p.toOuterMeasure_mono h).trans (p.toOuterMeasure_apply_le_toMeasure_apply t)

Premises used: PMF.toOuterMeasure_mono, PMF.toOuterMeasure_apply_le_toMeasure_apply, LE.le.trans
-- 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 ∩ p.support) : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(measure_mono s.inter_subset_left).antisymm (p.toMeasure_mono hs (refl _))

Premises used: LE.le.antisymm, Set.inter_subset_left, MeasureTheory.measure_mono, refl, PMF.toMeasure_mono
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
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∞)
⊢ Eq (α := Measure α) (Measure.restrict p.toMeasure p.support) p.toMeasure

Tactic:
ext s hs
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
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∞)
h₁ h₂ :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥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∞)

Tactic:
rw [Measure.restrict_apply hs, p.toMeasure_apply_inter_support hs]

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

Tactic:
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using
    p.toOuterMeasure_apply_eq_of_inter_support_eq h

Premises used: PMF.toOuterMeasure_apply_eq_of_inter_support_eq, PMF.toMeasure_apply_eq_toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
h : Eq (α := Measure α) p.toMeasure q.toMeasure
h₁ : ∀ (x : α), Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ p = q

Tactic:
ext x
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
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∞)
h₃ h₄ :
  Eq (α := ℝ≥0∞) (((q.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∞)

Tactic:
rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
    ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]

Premises used: PMF.toMeasure_apply_singleton, MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
p q : PMF α
⊢ Eq (α := Measure α) p.toMeasure q.toMeasure ↔ p = q

Tactic:
toMeasure_injective.eq_iff

Premises used: Function.Injective.eq_iff, PMF.toMeasure_injective
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
⊢ MeasurableSet (s ∩ p.support)

Tactic:
have hs := (p.support_countable.mono s.inter_subset_right).measurableSet
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet (s ∩ p.support)
rw :
  Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₃ rw₄ :
  Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : 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]

Premises used: Set.Countable.measurableSet, PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.support_countable, PMF.toOuterMeasure_apply_inter_support, MeasureTheory.Measure.restrict_apply', PMF.restrict_toMeasure_support
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Finset α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
    (∑ x ∈ s, (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(p.toMeasure_apply_eq_toOuterMeasure s).trans (p.toOuterMeasure_apply_finset s)

Premises used: SetLike.coe, PMF.toOuterMeasure_apply_finset, PMF.toMeasure_apply_eq_toOuterMeasure, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(p.toMeasure_apply_eq_toOuterMeasure s).trans (p.toOuterMeasure_apply s)

Premises used: PMF.toOuterMeasure_apply, PMF.toMeasure_apply_eq_toOuterMeasure, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
inst_1 : MeasurableSingletonClass α
s : Set α
inst_2 : Fintype α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ x : α, s.indicator (⇑p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
(p.toMeasure_apply_eq_toOuterMeasure s).trans (p.toOuterMeasure_apply_fintype s)

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure, Eq.trans, PMF.toOuterMeasure_apply_fintype
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
x : α
⊢ Eq (α := ℝ≥0∞) ((μ.toPMF : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑μ.toPMF : (a : α) → ℝ≥0∞) x)
    (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x)
⊢ Eq (α := ℝ≥0∞) (((μ.toPMF.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [μ.toPMF.toMeasure_apply hs, ← μ.tsum_indicator_apply_singleton s hs]

Premises used: PMF.toMeasure_apply, MeasureTheory.Measure.toPMF, MeasureTheory.Measure.tsum_indicator_apply_singleton
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑μ.toPMF : (a : α) → ℝ≥0∞) x)
    (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x)

Tactic:
rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
p : PMF α
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [MeasurableSet.univ, toMeasure_apply_eq_toOuterMeasure_apply, Set.indicator_univ,
      toOuterMeasure_apply, ENNReal.coe_eq_one] using tsum_coe p

Premises used: PMF.tsum_coe, ENNReal.coe_eq_one, PMF.toMeasure_apply_eq_toOuterMeasure_apply, Set.indicator_univ, PMF.toOuterMeasure_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
x : α
rw :
  Eq (α := ℝ≥0∞) ((Measure.toPMF p.toMeasure : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.toPMF p.toMeasure : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]

Premises used: PMF.toMeasure_apply_singleton, MeasurableSingletonClass.measurableSet_singleton, PMF.toMeasure, MeasureTheory.Measure.toPMF_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
rw : p.toMeasure = μ ↔ Eq (α := Measure α) p.toMeasure μ.toPMF.toMeasure
rw₁ rw₂ : p.toMeasure = μ ↔ p.toMeasure = μ
⊢ p.toMeasure = μ ↔ p = μ.toPMF

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Premises used: MeasureTheory.Measure.toPMF_toMeasure, PMF.toMeasure_inj
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
rw : Eq (α := Measure α) μ.toPMF.toMeasure p.toMeasure ↔ μ = p.toMeasure
rw₁ rw₂ : μ = p.toMeasure ↔ μ = p.toMeasure
⊢ μ.toPMF = p ↔ μ = p.toMeasure

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Premises used: MeasureTheory.Measure.toPMF_toMeasure, PMF.toMeasure_inj
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
norm_cast : Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0)) 1
⊢ Eq (α := ℝ≥0∞)
    (∑ a : Fin (n + 1),
      (↑(p ^ (↑a : ℕ) * (1 - p) ^ ((↑(Fin.last n) : ℕ) - (↑a : ℕ)) * (↑(n.choose (↑a : ℕ)) : ℝ≥0)) : ℝ≥0∞))
    1

Tactic:
norm_cast
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * (↑(n.choose m) : ℝ≥0) = (p + (1 - p)) ^ n

Tactic:
(add_pow p (1 - p) n).symm

Premises used: HSub.hSub, add_pow, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
h₁ :
  Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0))
    (∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * (↑(n.choose m) : ℝ≥0))
h₂ : 1 = (p + (1 - p)) ^ n
⊢ Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0)) 1

Tactic:
convert! (add_pow p (1 - p) n).symm

Premises used: HSub.hSub, add_pow, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
h₁ :
  Eq (α := ℝ≥0)
    (∑ i ∈ Finset.range (n + 1),
      if h : i < n + 1 then
        p ^ (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ) * (1 - p) ^ (n - (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) *
          (↑(n.choose (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) : ℝ≥0)
      else 0)
    (∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * (↑(n.choose m) : ℝ≥0))
⊢ Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0))
    (∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * (↑(n.choose m) : ℝ≥0))

Tactic:
rw [Finset.sum_fin_eq_sum_range]

Premises used: Finset.sum_fin_eq_sum_range
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
h₁ :
  ∀ x ∈ Finset.range (n + 1),
    (if h : x < n + 1 then
        p ^ (↑(⟨x, h⟩ : Fin (n + 1)) : ℕ) * (1 - p) ^ (n - (↑(⟨x, h⟩ : Fin (n + 1)) : ℕ)) *
          (↑(n.choose (↑(⟨x, h⟩ : Fin (n + 1)) : ℕ)) : ℝ≥0)
      else 0) =
      p ^ x * (1 - p) ^ (n - x) * (↑(n.choose x) : ℝ≥0)
⊢ Eq (α := ℝ≥0)
    (∑ i ∈ Finset.range (n + 1),
      if h : i < n + 1 then
        p ^ (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ) * (1 - p) ^ (n - (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) *
          (↑(n.choose (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) : ℝ≥0)
      else 0)
    (∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * (↑(n.choose m) : ℝ≥0))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i < n + 1

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
h₁ h₂ :
  p ^ (↑(⟨i, hi⟩ : Fin (n + 1)) : ℕ) * (1 - p) ^ (n - (↑(⟨i, hi⟩ : Fin (n + 1)) : ℕ)) *
      (↑(n.choose (↑(⟨i, hi⟩ : Fin (n + 1)) : ℕ)) : ℝ≥0) =
    p ^ i * (1 - p) ^ (n - i) * (↑(n.choose i) : ℝ≥0)
⊢ (if h : i < n + 1 then
      p ^ (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ) * (1 - p) ^ (n - (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) *
        (↑(n.choose (↑(⟨i, h⟩ : Fin (n + 1)) : ℕ)) : ℝ≥0)
    else 0) =
    p ^ i * (1 - p) ^ (n - i) * (↑(n.choose i) : ℝ≥0)

Tactic:
rw [dif_pos hi]

Premises used: dif_pos
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
h₁ : 1 = HPow.hPow (α := ℝ≥0) 1 n
h₂ h₃ : Eq (α := ℝ≥0) 1 1
⊢ 1 = (p + (1 - p)) ^ n

Tactic:
rw [add_tsub_cancel_of_le (mod_cast h), one_pow]

Premises used: one_pow, add_tsub_cancel_of_le
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
i : Fin (n + 1)
⊢ (binomial p h n : (a : Fin (n + 1)) → ℝ≥0∞) i =
    (↑p : ℝ≥0∞) ^ (↑i : ℕ) * (1 - (↑p : ℝ≥0∞)) ^ ((↑(Fin.last n) : ℕ) - (↑i : ℕ)) * (↑(n.choose (↑i : ℕ)) : ℝ≥0∞)

Tactic:
simp [binomial]

Premises used: PMF.binomial
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n : (a : Fin (n + 1)) → ℝ≥0∞) 0 = (1 - (↑p : ℝ≥0∞)) ^ n

Tactic:
simp [binomial_apply]

Premises used: PMF.binomial_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.last n) = (↑p : ℝ≥0∞) ^ n

Tactic:
simp [binomial_apply]

Premises used: PMF.binomial_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.last n) = (↑p : ℝ≥0∞) ^ n

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
h₁ :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    Eq (α := ℝ≥0∞) ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) i : ℝ≥0∞)
      ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := PMF (Fin (HAdd.hAdd (α := ℕ) 1 1))) (binomial p h 1)
    (map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h))

Tactic:
ext i
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h₁ :
  Eq (α := ℝ≥0∞)
    ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩) : ℝ≥0∞)
    ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩) :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩) : ℝ≥0∞)
    ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) i : ℝ≥0∞)
    ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
fin_cases i
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ Eq (α := ℝ≥0∞)
    ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩) : ℝ≥0∞)
    ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩) :
      ℝ≥0∞)

Tactic:
simp [binomial_apply]

Premises used: PMF.binomial_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ Eq (α := ℝ≥0∞)
    ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩) : ℝ≥0∞)
    ((map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h) : (a : Fin (1 + 1)) → ℝ≥0∞)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩) :
      ℝ≥0∞)

Tactic:
simp [binomial_apply]

Premises used: PMF.binomial_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ k % (b + 1) = k

Tactic:
simpa using Order.lt_add_one_iff.mpr hb

Premises used: Iff.mpr, Order.lt_add_one_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ k % (b + 1) = k

Tactic:
have eq0 : k % (b + 1) = k := by simpa using Order.lt_add_one_iff.mpr hb
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑(1 - x) : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
⊢ 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
⊢ 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))

Tactic:
have eq1 : 1 - (x : ℝ≥0∞) = ENNReal.ofReal (1 - x : ℝ) := by norm_cast
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
⊢ 1 - (↑x : ℝ) ≥ 0

Tactic:
simpa
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
⊢ 1 - (↑x : ℝ) ≥ 0

Tactic:
have : (1 - (x : ℝ)) ≥ 0 := by simpa
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
this : 1 - (↑x : ℝ) ≥ 0
hp : 0 ≤ (↑x : ℝ)
rwa : 0 ≤ (↑x : ℝ) ^ k
rwa₁ : 0 ≤ (↑x : ℝ) ^ k * (1 - (↑x : ℝ)) ^ (b - k)
⊢ ENNReal.ofReal ((↑(b.choose k) : ℝ) * (↑x : ℝ) ^ k * (1 - (↑x : ℝ)) ^ (b - k)) =
    (binomial x h b : (a : Fin (b + 1)) → ℝ≥0∞) (Fin.ofNat (b + 1) k)

Tactic:
rwa [Fin.ofNat_eq_cast, PMF.binomial_apply, Fin.val_natCast, Fin.val_last, eq0, eq1,
    coe_nnreal_eq x, mul_rotate, ofReal_mul, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_natCast]

Premises used: Fin.val_natCast, Fin.ofNat_eq_cast, ENNReal.ofReal_mul, PMF.binomial_apply, ENNReal.coe_nnreal_eq, ENNReal.ofReal_natCast, ENNReal.ofReal_pow, Fin.val_last, mul_rotate
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
this : 1 - (↑x : ℝ) ≥ 0
⊢ 0 ≤ (↑x : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
this : 1 - (↑x : ℝ) ≥ 0
⊢ 0 ≤ (↑x : ℝ) ^ k

Tactic:
positivity
-- Module: Mathlib.Probability.ProbabilityMassFunction.Binomial
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
this : 1 - (↑x : ℝ) ≥ 0
⊢ 0 ≤ (↑x : ℝ) ^ k * (1 - (↑x : ℝ)) ^ (b - k)

Tactic:
positivity