awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
this :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))

Tactic:
simpa [div_eq_mul_inv] using (hr.pow k).mul_const ((k.factorial : ℝ)⁻¹)

Premises used: Filter.Tendsto.mul_const, Filter.Tendsto.pow, div_eq_mul_inv, Nat.cast, Inv.inv, Nat.factorial
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
rw :
  Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (r ^ k / (↑k.factorial : ℝ) * Real.exp (-r)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (Real.exp (-r) * r ^ k / (↑k.factorial : ℝ)))

Tactic:
rw [mul_div_assoc, mul_comm]

Premises used: mul_div_assoc, mul_comm
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (r ^ k / (↑k.factorial : ℝ) * Real.exp (-r)))

Tactic:
(tendsto_choose_mul_pow_atTop k hr).mul ?_

Premises used: ProbabilityTheory.tendsto_choose_mul_pow_atTop, Filter.Tendsto.mul
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
refine : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (r ^ k / (↑k.factorial : ℝ) * Real.exp (-r)))

Tactic:
refine (tendsto_choose_mul_pow_atTop k hr).mul ?_

Premises used: ProbabilityTheory.tendsto_choose_mul_pow_atTop, Filter.Tendsto.mul
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ ∀ᶠ (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))
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
h : ∀ (n : ℕ) (hn : k ≤ n) (hne : p n < 1 / 2), (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
filter_upwards [eventually_ge_atTop k, hp_lt_half] with n hn hne

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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 ≠ 0

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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
h h₁ : (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹ = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
⊢ (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
rw [pow_sub₀ _ (by grind) hn]

Premises used: pow_sub₀
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹

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]
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)))

Tactic:
Tendsto.congr' hEq.symm ?_

Premises used: Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹
refine : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r)))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))

Tactic:
refine Tendsto.congr' hEq.symm ?_

Premises used: Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹
⊢ Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹
⊢ Real.exp (-r) = Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹

Tactic:
have : Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹ := by field
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹
rw : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r)))

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹))

Tactic:
Tendsto.mul (Real.tendsto_one_add_pow_exp_of_tendsto ?_) ?_

Premises used: Real.tendsto_one_add_pow_exp_of_tendsto, Filter.Tendsto.mul
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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))
refine_2 : Tendsto (fun (n : ℕ) ↦ ((1 - p n) ^ k)⁻¹) atTop (𝓝 (HPow.hPow (α := ℝ) 1 k)⁻¹)
⊢ Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (HPow.hPow (α := ℝ) 1 k)⁻¹))

Tactic:
refine Tendsto.mul (Real.tendsto_one_add_pow_exp_of_tendsto ?_) ?_

Premises used: Real.tendsto_one_add_pow_exp_of_tendsto, Filter.Tendsto.mul
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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 : ℕ) ↦ (↑n : ℝ) * -p n) atTop (𝓝 (-r))

Tactic:
simpa using hr.neg

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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)⁻¹
⊢ HPow.hPow (α := ℝ) 1 k ≠ 0

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 1 - p n) atTop (𝓝 1)
⊢ Tendsto (fun (n : ℕ) ↦ ((1 - p n) ^ k)⁻¹) atTop (𝓝 (HPow.hPow (α := ℝ) 1 k)⁻¹)

Tactic:
refine Tendsto.inv₀ (.pow ?_ k) (by simp)

Premises used: Filter.Tendsto.pow, Filter.Tendsto.inv₀
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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) atTop (𝓝 1)

Tactic:
simpa using tendsto_const_nhds.sub (tendsto_zero_of_tendsto_mul_atTop hr)

Premises used: tendsto_const_nhds, ProbabilityTheory.tendsto_zero_of_tendsto_mul_atTop, Filter.Tendsto.sub
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0) * p n) atTop (𝓝 r)
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 : ℝ))))
⊢ 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:
simp_rw [poissonMeasure_singleton]

Premises used: ProbabilityTheory.poissonMeasure_singleton
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Tendsto (fun (a : ℕ) ↦ (↑a : ℝ≥0) * p a) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * (↑(p n) : ℝ)) atTop (𝓝 (↑r : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
k : ℕ
r : ℝ≥0
p : ℕ → ℝ≥0
h : ∀ (n : ℕ), p n ≤ 1
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0) * p n) atTop (𝓝 r)
⊢ 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:
exact tendsto_ofReal (tendsto_choose_mul_pow_of_tendsto_mul_atTop k (by norm_cast))

Premises used: ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop, ENNReal.tendsto_ofReal
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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∞)

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))
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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∞)

Tactic:
Tendsto.congr' ?_ t1

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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∞)
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) ⋯ n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.ofNat (n + 1) k)
⊢ 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∞)

Tactic:
refine Tendsto.congr' ?_ t1

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
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∞)
⊢ EventuallyEq (β := ℝ≥0∞) atTop
    (fun (n : ℕ) ↦ ENNReal.ofReal ((↑(n.choose k) : ℝ) * (↑(p n) : ℝ) ^ k * (1 - (↑(p n) : ℝ)) ^ (n - k))) fun (n : ℕ) ↦
    (PMF.binomial (p n) ⋯ n : (a : Fin (n + 1)) → ℝ≥0∞) (Fin.ofNat (n + 1) k)

Tactic:
simpa only [EventuallyEq, eventually_atTop, ge_iff_le] using
    ⟨k, fun b hb ↦ PMF.binomial_apply_of_le hb (h b)⟩

Premises used: ge_iff_le, Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
X Y : Ω → Set ι
s u : Set ι
i j : ι
p q : (↑I : Type)
P : Measure Ω
⊢ IsProbabilityMeasure setBer(u, p)

Tactic:
MeasurableEquiv.setOf.symm.measurableEmbedding.isProbabilityMeasure_comap <| .of_forall fun P ↦
    ⟨{i | P i}, rfl⟩

Premises used: MeasurableEquiv.measurableEmbedding, Set.Mem, ProbabilityTheory.setBernoulli, setOf, MeasurableEquiv.setOf, MeasurableEquiv.symm, Filter.Eventually.of_forall, Exists.intro, MeasurableEmbedding.isProbabilityMeasure_comap, rfl
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
⊢ setBer(u, p) =
    map (fun (p : ι → Prop) ↦ {i : ι | p i})
      (infinitePi (X := fun (a : ι) ↦ Prop) fun (i : ι) ↦
        HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
          HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False))

Tactic:
MeasurableEquiv.setOf.comap_symm

Premises used: Set.Mem, ProbabilityTheory.setBernoulli, setOf, MeasurableEquiv.setOf, MeasurableEquiv.comap_symm
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) 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∞)
        ((fun (t : Set ι) (i : ι) ↦ i ∈ t) '' S) :
      ℝ≥0∞)

Tactic:
MeasurableEquiv.setOf.symm.measurableEmbedding.comap_apply ..

Premises used: MeasurableEquiv.measurableEmbedding, Set.Mem, MeasurableEquiv.setOf, MeasurableEquiv.symm, MeasurableEmbedding.comap_apply
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) 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∞)
        ((fun (p : (i : ι) → Prop) ↦ {i : ι | p i}) ⁻¹' S) :
      ℝ≥0∞)

Tactic:
MeasurableEquiv.setOf.symm.comap_apply ..

Premises used: Set.Mem, MeasurableEquiv.comap_apply, setOf, MeasurableEquiv.setOf, MeasurableEquiv.symm
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
⊢ setBer(u, 0) = dirac ∅

Tactic:
simp [setBernoulli_eq_map]

Premises used: ProbabilityTheory.setBernoulli_eq_map
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
⊢ setBer(u, 1) = dirac u

Tactic:
simp [setBernoulli_eq_map]

Premises used: ProbabilityTheory.setBernoulli_eq_map
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
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

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]

Premises used: Set.setOf_and, Set.not_subset_iff_exists_mem_notMem, Filter.Eventually, MeasureTheory.measure_iUnion_null_iff, Set.setOf_exists, MeasureTheory.mem_ae_iff, Set.compl_setOf
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞)
neg :
  ∀ (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∞)

Tactic:
by_cases hi : i ∈ u
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞)

Tactic:
simp [*]
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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} ∩ {s : Set ι | i ∉ u}) : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)

Tactic:
simp [hi]
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
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∞)
⊢ 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:
rw [setBernoulli_apply']

Premises used: ProbabilityTheory.setBernoulli_apply'
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
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})
⊢ 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:
congr!
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
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
⊢ 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:
ext
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
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:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [infinitePi_cylinder, hi]

Premises used: MeasureTheory.Measure.infinitePi_cylinder