awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
have hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
Tactic: have hp_lt_half : ∀ᶠ n in atTop, p n < 1 / 2 :=
    (tendsto_zero_of_tendsto_mul_atTop hr).eventually (Iio_mem_nhds (by norm_num))
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
have h : ∀ (n : ℕ) (hn : k ≤ n) (hne : p n < 1 / 2), (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
Tactic: filter_upwards [eventually_ge_atTop k, hp_lt_half] with n hn hne
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
have h : (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹ = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
Tactic: rw [pow_sub₀ _ (by grind) hn]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
have hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
Tactic: have hEq : (fun n => (1 - p n) ^ (n - k)) =ᶠ[atTop]
      (fun n => (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) := by
    filter_upwards [eventually_ge_atTop k, hp_lt_half] with n hn hne
    rw [pow_sub₀ _ (by grind) hn]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
have refine : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r)))
Tactic: refine Tendsto.congr' hEq.symm ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r)))
have this : Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹
Tactic: have : Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹ := by field
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r)))
have rw : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹))
have refine_1 : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * -p n) atTop (𝓝 (-r))
Tactic: refine Tendsto.mul (Real.tendsto_one_add_pow_exp_of_tendsto ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹
refine_1 : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * -p n) atTop (𝓝 (-r))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹))
have refine_2 : Tendsto (fun (n : ℕ) ↦ ((1 - p n) ^ k)⁻¹) atTop (𝓝 (HPow.hPow (α := ℝ) 1 k)⁻¹)
Tactic: refine Tendsto.mul (Real.tendsto_one_add_pow_exp_of_tendsto ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ ((1 - p n) ^ k)⁻¹) atTop (𝓝 (HPow.hPow (α := ℝ) 1 k)⁻¹)
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 1 - p n) atTop (𝓝 1)
Tactic: refine Tendsto.inv₀ (.pow ?_ k) (by simp)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0) * p n) atTop (𝓝 r)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) atTop
    (𝓝 ((Po(r) : (a : Set ℕ) → ℝ≥0∞) {k}) : Filter ℝ≥0∞)
have simp_rw : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) atTop
  (𝓝 (ENNReal.ofReal (Real.exp (-(↑r : ℝ)) * (↑r : ℝ) ^ k / (↑k.factorial : ℝ))))
Tactic: simp_rw [poissonMeasure_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0) * p n) atTop (𝓝 r)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((PMF.binomial (p n) ⋯ n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.ofNat (n + 1) k) : ℝ≥0∞))
    atTop (𝓝 ((Po(r) : (a : Set ℕ) → ℝ≥0∞) {k}) : Filter ℝ≥0∞)
have t1 : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) atTop
  (𝓝 ((Po(r) : (a : Set ℕ) → ℝ≥0∞) {k}) : Filter ℝ≥0∞)
Tactic: have t1 : Tendsto (fun n => (ENNReal.ofReal (n.choose k * (p n) ^ k * (1 - p n) ^ (n - k) : ℝ)))
      atTop (𝓝 (poissonMeasure r {k})) := by
    simp_rw [poissonMeasure_singleton]
    exact tendsto_ofReal (tendsto_choose_mul_pow_of_tendsto_mul_atTop k (by norm_cast))
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0) * p n) atTop (𝓝 r)
t1 :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) atTop
    (𝓝 ((Po(r) : (a : Set ℕ) → ℝ≥0∞) {k}) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((PMF.binomial (p n) ⋯ n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.ofNat (n + 1) k) : ℝ≥0∞))
    atTop (𝓝 ((Po(r) : (a : Set ℕ) → ℝ≥0∞) {k}) : Filter ℝ≥0∞)
have refine : EventuallyEq (β := ℝ≥0∞) atTop
  (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) fun (n : ℕ) ↦
  (PMF.binomial (p n) sorry n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.ofNat (n + 1) k)
Tactic: refine Tendsto.congr' ?_ t1
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u
have simp : ∀ (i : ι),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: simp only [Filter.Eventually, mem_ae_iff, Set.compl_setOf, Set.not_subset_iff_exists_mem_notMem,
    Set.setOf_exists, Set.setOf_and, measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos : ∀ (hi : i ∈ u),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: by_cases hi : i ∈ u
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
pos :
  ∀ (hi : i ∈ u),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : ∀ (hi : i ∉ u),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: by_cases hi : i ∈ u
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
            HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
              HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
          Measure ((i : ι) → Prop)) :
        (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
      (Set.preimage (β := Set ι) (fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) {s : Set ι | i ∈ s}) :
    ℝ≥0∞)
  (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
            HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
              HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
          Measure ((i : ι) → Prop)) :
        (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
      (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
    ℝ≥0∞)
Tactic: rw [setBernoulli_apply']
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
⊢ Eq (α := ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (Set.preimage (β := Set ι) (fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) {s : Set ι | i ∈ s}) :
      ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
have h : Eq (α := Set ((i : ι) → Prop))
  (Set.preimage (β := Set ι) (fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) {s : Set ι | i ∈ s})
  (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True})
Tactic: congr!
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
⊢ Eq (α := Set ((i : ι) → Prop))
    (Set.preimage (β := Set ι) (fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) {s : Set ι | i ∈ s})
    (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True})
have h : ∀ (x : (i : ι) → Prop),
  Membership.mem (γ := Set ((i : ι) → Prop))
      (Set.preimage (β := Set ι) (fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) {s : Set ι | i ∈ s}) x ↔
    Membership.mem (γ := Set ((i : ι) → Prop)) (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have i₁ : Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({s : Set ι | i ∈ s} ∩ {s : Set ι | i ∉ u}) : ℝ≥0∞)
  ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
Tactic: calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
i₁ :
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({s : Set ι | i ∈ s} ∩ {s : Set ι | i ∉ u}) : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have i₂ : Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
  (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
            HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
              HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
          Measure ((i : ι) → Prop)) :
        (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
      (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
    ℝ≥0∞)
Tactic: calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
i₁ :
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({s : Set ι | i ∈ s} ∩ {s : Set ι | i ∉ u}) : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
i₂ :
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have i₃ : Eq (α := ℝ≥0∞)
  (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
            HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
              HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
          Measure ((i : ι) → Prop)) :
        (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
      (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u
have simp : ∀ (i : ι),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: classical
  simp only [Filter.Eventually, mem_ae_iff, Set.compl_setOf, Set.not_subset_iff_exists_mem_notMem,
    Set.setOf_exists, Set.setOf_and, measure_iUnion_null_iff]
  rintro i
  by_cases hi : i ∈ u
  · simp [*]
  calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
simp simp₁ :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u
have pos : ∀ (i : ι) (hi : i ∈ u),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: classical
  simp only [Filter.Eventually, mem_ae_iff, Set.compl_setOf, Set.not_subset_iff_exists_mem_notMem,
    Set.setOf_exists, Set.setOf_and, measure_iUnion_null_iff]
  rintro i
  by_cases hi : i ∈ u
  · simp [*]
  calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
simp simp₁ :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
pos :
  ∀ (i : ι) (hi : i ∈ u),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u
have neg : ∀ (i : ι) (hi : i ∉ u),
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: classical
  simp only [Filter.Eventually, mem_ae_iff, Set.compl_setOf, Set.not_subset_iff_exists_mem_notMem,
    Set.setOf_exists, Set.setOf_and, measure_iUnion_null_iff]
  rintro i
  by_cases hi : i ∈ u
  · simp [*]
  calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
inst : Countable ι
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) S : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | s ∈ S ∧ s ⊆ u} : ℝ≥0∞)
have apply : Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) (S \ {s : Set ι | s ∈ S ∧ s ⊆ u}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply (measure_eq_measure_of_null_diff (by grind) ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s u : Set ι
p : (↑I : Type)
inst : Countable ι
hsu : s ⊆ u
hu : u.Finite
⊢ (setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ (u \ s).ncard
have lift : ∀ (u : Finset ι) (hsu : s ⊆ (↑u : Set ι)),
  (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
Tactic: lift u to Finset ι using hu
Cleared hypotheses: u, hsu, hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
⊢ Eq (α := ℝ≥0∞)
    (∏' (i : ι),
      ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)))
    (∏ i ∈ u, if i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞))
have rw : ∀ x ∈ u,
  ((if x ∈ u ↔ x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if x ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) =
    if x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞)
Tactic: rw [tprod_eq_prod, Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
rw :
  ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if x ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) =
      if x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∏' (i : ι),
      ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)))
    (∏ i ∈ u, if i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞))
have rw₁ : ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if b ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) = 1
Tactic: rw [tprod_eq_prod, Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
⊢ (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
have _ : Eq (α := ℝ≥0∞) ((setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} : ℝ≥0∞)
  (∏' (i : ι),
      ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) :
    ℝ≥0∞)
Tactic: calc
    setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.setOf_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_setOf, Set.diff_eq_compl_inter, Set.inter_comm]