awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw :
  Eq (α := ℝ≥0∞) (((Measure.restrict p.toMeasure p.support : Measure α) : (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∞)
have rw₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥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]
-- 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)
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∞)
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (s ∩ p.support) : ℝ≥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]
-- 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)
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∞)
⊢ Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((p.toOuterMeasure : (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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ.toPMF.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (⇑μ.toPMF : (a : α) → ℝ≥0∞) x)
  (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x)
Tactic: rw [μ.toPMF.toMeasure_apply hs, ← μ.tsum_indicator_apply_singleton s hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
x : α
⊢ Eq (α := ℝ≥0∞) ((Measure.toPMF p.toMeasure : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((Measure.toPMF p.toMeasure : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
Tactic: rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.toPMF p.toMeasure : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
Tactic: rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p = μ.toPMF
have rw : p.toMeasure = μ ↔ Eq (α := Measure α) p.toMeasure μ.toPMF.toMeasure
Tactic: rw [← toMeasure_inj, Measure.toPMF_toMeasure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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
⊢ p.toMeasure = μ ↔ p = μ.toPMF
have rw₁ : p.toMeasure = μ ↔ p.toMeasure = μ
Tactic: rw [← toMeasure_inj, Measure.toPMF_toMeasure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst_3 : IsProbabilityMeasure μ
⊢ μ.toPMF = p ↔ μ = p.toMeasure
have rw : Eq (α := Measure α) μ.toPMF.toMeasure p.toMeasure ↔ μ = p.toMeasure
Tactic: rw [← toMeasure_inj, Measure.toPMF_toMeasure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
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
⊢ μ.toPMF = p ↔ μ = p.toMeasure
have rw₁ : μ = p.toMeasure ↔ μ = p.toMeasure
Tactic: rw [← toMeasure_inj, Measure.toPMF_toMeasure]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ Eq (α := ℝ≥0∞)
    (∑ a : Fin (n + 1),
      (↑(p ^ (↑a : ℕ) * (1 - p) ^ ((↑(Fin.last n) : ℕ) - (↑a : ℕ)) * (↑(n.choose (↑a : ℕ)) : ℝ≥0)) : ℝ≥0∞))
    1
have norm_cast : Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0)) 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0)) 1
have 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))
Tactic: convert! (add_pow p (1 - p) n).symm
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
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))
⊢ Eq (α := ℝ≥0) (∑ x : Fin (n + 1), p ^ (↑x : ℕ) * (1 - p) ^ (n - (↑x : ℕ)) * (↑(n.choose (↑x : ℕ)) : ℝ≥0)) 1
have h₂ : 1 = (p + (1 - p)) ^ n
Tactic: convert! (add_pow p (1 - p) n).symm
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 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))
have 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))
Tactic: rw [Finset.sum_fin_eq_sum_range]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 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))
have 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)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (hypothesis)
Goal:
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : 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) =
    p ^ i * (1 - p) ^ (n - i) * (↑(n.choose i) : ℝ≥0)
have hi₁ : i < n + 1
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < 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) =
    p ^ i * (1 - p) ^ (n - i) * (↑(n.choose i) : ℝ≥0)
have 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)
Tactic: rw [dif_pos hi]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n
have h₁ : 1 = HPow.hPow (α := ℝ≥0) 1 n
Tactic: rw [add_tsub_cancel_of_le (mod_cast h), one_pow]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
n : ℕ
h₁ : 1 = HPow.hPow (α := ℝ≥0) 1 n
⊢ 1 = (p + (1 - p)) ^ n
have h₂ : Eq (α := ℝ≥0) 1 1
Tactic: rw [add_tsub_cancel_of_le (mod_cast h), one_pow]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ Eq (α := PMF (Fin (HAdd.hAdd (α := ℕ) 1 1))) (binomial p h 1)
    (map (fun (x : Bool) ↦ bif x then 1 else 0) (bernoulli p h))
have 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∞)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
p : ℝ≥0
h : p ≤ 1
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∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩) : ℝ≥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, sorry⟩) :
    ℝ≥0∞)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
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∞)
⊢ 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∞)
have h₂ : Eq (α := ℝ≥0∞)
  ((binomial p h 1 : (a : Fin (1 + 1)) → ℝ≥0∞) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩) : ℝ≥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, sorry⟩) :
    ℝ≥0∞)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (hypothesis)
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ 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)
have eq0 : k % (b + 1) = k
Tactic: have eq0 : k % (b + 1) = k := by simpa using Order.lt_add_one_iff.mpr hb
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
⊢ 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
have norm_cast : (↑(1 - x) : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (hypothesis)
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = 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)
have eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
Tactic: have eq1 : 1 - (x : ℝ≥0∞) = ENNReal.ofReal (1 - x : ℝ) := by norm_cast
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (hypothesis)
Goal:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - (↑x : ℝ≥0∞) = ENNReal.ofReal (1 - (↑x : ℝ))
⊢ 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)
have this : 1 - (↑x : ℝ) ≥ 0
Tactic: have : (1 - (x : ℝ)) ≥ 0 := by simpa
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
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
⊢ 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)
have hp : 0 ≤ (↑x : ℝ)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
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 : ℝ)
⊢ 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)
have rwa : 0 ≤ (↑x : ℝ) ^ 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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Binomial (goal)
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
⊢ 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)
have rwa₁ : 0 ≤ (↑x : ℝ) ^ k * (1 - (↑x : ℝ)) ^ (b - 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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) (∑' (a : α), if f a ∈ s then (p : (a : α) → ℝ≥0∞) a else 0)
  (∑' (x : α), if x ∈ f ⁻¹' s then (p : (a : α) → ℝ≥0∞) x else 0)
Tactic: simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [toMeasure_apply_eq_toOuterMeasure_apply _ hs,
    toMeasure_apply_eq_toOuterMeasure_apply _ (measurableSet_preimage hf hs)]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
⊢ Eq (α := Measure β) (Measure.map f p.toMeasure) (map f p).toMeasure
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs : 1
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ Eq (α := ℝ≥0∞) ((q.seq p : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    (∑' (f : α → β) (a : α),
        if b = f a then
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        else 0 :
      ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  (∑' (a : α → β),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (a_1 : α), if b = a a_1 then (p : (a : α) → ℝ≥0∞) a_1 else 0 : ℝ≥0∞))
  (∑' (f : α → β) (a : α),
    if b = f a then
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    else 0)
Tactic: simp only [seq, mul_boole, bind_apply, pure_apply]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α → β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (a_1 : α), if b = a a_1 then (p : (a : α) → ℝ≥0∞) a_1 else 0 : ℝ≥0∞))
    (∑' (f : α → β) (a : α),
      if b = f a then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      else 0)
have refine : ∀ (f : α → β) (a : α),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞)
      (if b = f a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) =
    if b = f a then
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    else 0
Tactic: refine tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
⊢ map g (ofFintype f h) = ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) ⋯
have h₁ : ∀ (b : β),
  Eq (α := ℝ≥0∞) ((map g (ofFintype f h) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    ((ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) sorry : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: ext b : 1
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
b : β
⊢ Eq (α := ℝ≥0∞) ((map g (ofFintype f h) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    ((ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (∑' (a : α), if b = g a then f a else 0) (∑ a : α, if b = g a then f a else 0)
Tactic: simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]
-- 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 : α
⊢ (p.filter s h : (a : α) → ℝ≥0∞) a =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
have rw : (normalize (s.indicator (⇑p : (a : α) → ℝ≥0∞)) sorry sorry : (a : α) → ℝ≥0∞) a =
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
Tactic: rw [filter, normalize_apply]
-- 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 :
  (normalize (s.indicator (⇑p : (a : α) → ℝ≥0∞)) ⋯ ⋯ : (a : α) → ℝ≥0∞) a =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
⊢ (p.filter s h : (a : α) → ℝ≥0∞) a =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
have rw₁ : HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x)⁻¹ =
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
Tactic: rw [filter, normalize_apply]
-- 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
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (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]