awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
refine_2 refine_2₁ : ∀ a ∉ s, Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 0
⊢ PMF α

Tactic:
classical
  refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
  · simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
    have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
    exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card
  · exact fun x hx => by simp only [hx, if_false]

Premises used: Finset.sum_ite_mem, Finset.inter_self, ENNReal.natCast_ne_top, Finset.card, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
⊢ Eq (α := ℝ≥0∞) ((uniformOfFinset s hs : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ Eq (α := ℝ≥0∞) ((uniformOfFinset s hs : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((↑(#s) : ℝ≥0∞)⁻¹ : ℝ≥0∞)

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞) ((uniformOfFinset s hs : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
let : ∀ (a : α) (ha : a ∈ s) (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ (↑s : Set α)
⊢ ∀ (x : α), x ∈ (uniformOfFinset s hs).support ↔ x ∈ (↑s : Set α)

Tactic:
let ⟨a, ha⟩ := hs
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ (↑s : Set α)

Tactic:
simp [mem_support_iff]

Premises used: PMF.mem_support_iff
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
⊢ a ∈ (uniformOfFinset s hs).support ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
simp_rw :
  Eq (α := ℝ≥0∞) (if x ∈ t then if x ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 else 0)
    (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0)
simp_rw₁ :
  Eq (α := ℝ≥0∞) (if x ∈ t ∧ x ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0) (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0)
⊢ Eq (α := ℝ≥0∞) (if x ∈ t then (uniformOfFinset s hs : (a : α) → ℝ≥0∞) x else 0 : ℝ≥0∞)
    (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)

Tactic:
simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]

Premises used: and_comm, PMF.uniformOfFinset_apply, ite_and
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ {x ∈ s | x ∈ t}
⊢ x ∈ s ∧ x ∈ t

Tactic:
simpa using hx
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ {x ∈ s | x ∈ t}
⊢ x ∈ s ∧ x ∈ t

Tactic:
have this : x ∈ s ∧ x ∈ t := by simpa using hx
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ {x ∈ s | x ∈ t}
this : x ∈ s ∧ x ∈ t
⊢ Eq (α := ℝ≥0∞) (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0) (↑(#s) : ℝ≥0∞)⁻¹

Tactic:
simp only [this, and_self_iff, if_true]

Premises used: if_true, and_self_iff
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
⊢ ∑ x ∈ s with x ∈ t, (↑(#s) : ℝ≥0∞)⁻¹ = HDiv.hDiv (α := ℝ≥0∞) (↑(#({x ∈ s | x ∈ t})) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)

Tactic:
simp only [div_eq_mul_inv, Finset.sum_const, nsmul_eq_mul]

Premises used: div_eq_mul_inv, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
inst : MeasurableSpace α
ht : MeasurableSet t
⊢ (((uniformOfFinset s hs).toMeasure : MeasureTheory.Measure α) : (a : Set α) → ℝ≥0∞) t =
    HDiv.hDiv (α := ℝ≥0∞) (↑(#({x ∈ s | x ∈ t})) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_uniformOfFinset_apply hs t)

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_uniformOfFinset_apply, Eq.trans
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
a : α
⊢ Eq (α := ℝ≥0∞) ((uniformOfFintype α : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((↑(Fintype.card α) : ℝ≥0∞)⁻¹ : ℝ≥0∞)

Tactic:
simp [uniformOfFintype, Finset.mem_univ, uniformOfFinset_apply]

Premises used: Finset.mem_univ, PMF.uniformOfFintype, PMF.uniformOfFinset_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_2
inst : Fintype α
inst_1 : Nonempty α
x : α
⊢ x ∈ (uniformOfFintype α).support ↔ Membership.mem (γ := Set α) ⊤ x

Tactic:
simp [mem_support_iff]

Premises used: PMF.mem_support_iff
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
a : α
⊢ a ∈ (uniformOfFintype α).support

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₂ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₃ rw₄ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)

Tactic:
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]

Premises used: Finset.card_univ, PMF.uniformOfFintype, Fintype.card_subtype, PMF.toOuterMeasure_uniformOfFinset_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₂ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₃ rw₄ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)

Tactic:
classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]

Premises used: Finset.card_univ, PMF.uniformOfFintype, Fintype.card_subtype, PMF.toOuterMeasure_uniformOfFinset_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : MeasurableSpace α
hs : MeasurableSet s
inst_3 : Fintype (↑s : Type u_1)
⊢ (((uniformOfFintype α).toMeasure : MeasureTheory.Measure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)

Tactic:
simp [uniformOfFintype, Fintype.card_subtype, hs]

Premises used: PMF.uniformOfFintype, Fintype.card_subtype
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : MeasurableSpace α
hs : MeasurableSet s
inst_3 : Fintype (↑s : Type u_1)
⊢ (((uniformOfFintype α).toMeasure : MeasureTheory.Measure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)

Tactic:
classical
  simp [uniformOfFintype, Fintype.card_subtype, hs]

Premises used: PMF.uniformOfFintype, Fintype.card_subtype
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
simp_rw :
  ∑' (b : α), HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(Multiset.count b s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑' (b : α), (↑(Multiset.count b s) : ℝ≥0∞))
⊢ ∑' (b : α), HDiv.hDiv (α := ℝ≥0∞) (↑(Multiset.count b s) : ℝ≥0∞) (↑s.card : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑' (b : α), (↑(Multiset.count b s) : ℝ≥0∞))

Tactic:
simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s.toFinset
rwa : a ∉ s
rwa₁ rwa₂ rwa₃ rwa₄ : a ∉ s.toFinset
⊢ Multiset.count a s = 0

Tactic:
rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]

Premises used: Multiset.count_eq_zero, Multiset.mem_toFinset
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
rw : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(∑ x ∈ s.toFinset, Multiset.count x s) : ℝ≥0∞) = 1
rw₁ : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑s.card : ℝ≥0∞) = 1
rw₂ rw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑ b ∈ s.toFinset, (↑(Multiset.count b s) : ℝ≥0∞)) = 1

Tactic:
rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
            ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)]

Premises used: Iff.mpr, Multiset.card_eq_zero, Multiset.toFinset_sum_count_eq, ENNReal.natCast_ne_top, Function.comp, Nat.cast_sum, Iff.mp, ENNReal.inv_mul_cancel, Nat.cast_ne_zero
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
⊢ (ofMultiset s hs : (a : α) → ℝ≥0∞) a = HDiv.hDiv (α := ℝ≥0∞) (↑(Multiset.count a s) : ℝ≥0∞) (↑s.card : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ ∀ (x : α), x ∈ (ofMultiset s hs).support ↔ x ∈ (↑s.toFinset : Set α)

Tactic:
simp [mem_support_iff]

Premises used: PMF.mem_support_iff
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
⊢ a ∈ (ofMultiset s hs).support ↔ a ∈ s.toFinset

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞) ((ofMultiset s hs : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero,
    ENNReal.natCast_ne_top, or_false] using ha

Premises used: ENNReal.natCast_ne_top, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, or_false, Multiset.count_eq_zero, PMF.ofMultiset_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (∑' (x : α), t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x)
    (∑' (i : α),
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count i (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹)
⊢ ((ofMultiset s hs).toOuterMeasure : (a : Set α) → ℝ≥0∞) t =
    HDiv.hDiv (α := ℝ≥0∞) (∑' (x : α), (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞))
      (↑s.card : ℝ≥0∞)

Tactic:
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]

Premises used: ENNReal.tsum_mul_right, div_eq_mul_inv, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x)
    (∑' (i : α),
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count i (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹)

Tactic:
tsum_congr fun x => ?_

Premises used: tsum_congr
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
refine :
  ∀ (x : α),
    t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x)
    (∑' (i : α),
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count i (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹)

Tactic:
refine tsum_congr fun x => ?_

Premises used: tsum_congr
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
pos :
  ∀ (hx : x ∈ t),
    t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
neg :
  ∀ (hx : x ∉ t),
    t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
⊢ t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∈ t
⊢ t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹

Tactic:
simp [Set.indicator, hx, div_eq_mul_inv]

Premises used: Set.indicator, div_eq_mul_inv
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∉ t
⊢ t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹

Tactic:
simp [Set.indicator, hx, div_eq_mul_inv]

Premises used: Set.indicator, div_eq_mul_inv
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
inst : MeasurableSpace α
ht : MeasurableSet t
⊢ (((ofMultiset s hs).toMeasure : MeasureTheory.Measure α) : (a : Set α) → ℝ≥0∞) t =
    HDiv.hDiv (α := ℝ≥0∞) (∑' (x : α), (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞))
      (↑s.card : ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_ofMultiset_apply hs t)

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_ofMultiset_apply, Eq.trans
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
rw :
  Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | p (X ω)} : ℝ≥0∞)
    ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x : 𝓧 | p x}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | p (X ω)} : ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) {x : 𝓧 | p x} : ℝ≥0∞)

Tactic:
rw [← hX.map_eq, map_apply_of_aemeasurable hX.aemeasurable hp]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
⊢ Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | p (X ω)} : ℝ≥0∞)
    ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x : 𝓧 | p x}) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
rw : P.real {ω : Ω | p (X ω)} = P.real (X ⁻¹' {x : 𝓧 | p x})
⊢ P.real {ω : Ω | p (X ω)} = μ.real {x : 𝓧 | p x}

Tactic:
rw [← hX.map_eq, map_measureReal_apply_of_aemeasurable hX.aemeasurable hp]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, MeasureTheory.map_measureReal_apply_of_aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
⊢ P.real {ω : Ω | p (X ω)} = P.real (X ⁻¹' {x : 𝓧 | p x})

Tactic:
simp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
rw₂ : map f μ = ν
rw₃ : map f (map X P) = ν
rw₄ : map (f ∘ X) P = ν
rw₅ : map (fun (x : Ω) ↦ f (X x)) P = ν
rw₆ rw₇ : ν = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν

Tactic:
rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, Function.comp_def, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X Y : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
hY : Y =ᶠ[ae P] X
rw : map X P = μ
rw₁ rw₂ : μ = μ
⊢ map Y P = μ

Tactic:
rw [map_congr hY, hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq, MeasureTheory.Measure.map_congr
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : Measurable p
rw : (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂map X P, p x
rw₁ rw₂ : (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : Ω) ∂P, p (X x)
⊢ (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂μ, p x

Tactic:
rw [← hX.map_eq, ae_map_iff hX.aemeasurable (measurableSet_setOf.2 hp)]

Premises used: Iff.mpr, measurableSet_setOf, MeasureTheory.ae_map_iff, ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
rw : IsFiniteMeasure P ↔ IsFiniteMeasure (m0 := m𝓧) (map X P)
rw₁ rw₂ : IsFiniteMeasure P ↔ IsFiniteMeasure P
⊢ IsFiniteMeasure P ↔ IsFiniteMeasure μ

Tactic:
rw [← hX.map_eq, isFiniteMeasure_map_iff hX.aemeasurable]

Premises used: MeasureTheory.Measure.isFiniteMeasure_map_iff, ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
rw : IsProbabilityMeasure P ↔ IsProbabilityMeasure (m0 := m𝓧) (map X P)
rw₁ rw₂ : IsProbabilityMeasure P ↔ IsProbabilityMeasure P
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure μ

Tactic:
rw [← hX.map_eq, isProbabilityMeasure_map_iff hX.aemeasurable]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, MeasureTheory.Measure.isProbabilityMeasure_map_iff
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure μ
hX : HasLaw X μ P
⊢ IsFiniteMeasure P

Tactic:
hX.isFiniteMeasure_iff.2 ‹_›

Premises used: Iff.mpr, ProbabilityTheory.HasLaw.isFiniteMeasure_iff
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsProbabilityMeasure μ
hX : HasLaw X μ P
⊢ IsProbabilityMeasure P

Tactic:
hX.isProbabilityMeasure_iff.2 ‹_›

Premises used: Iff.mpr, ProbabilityTheory.HasLaw.isProbabilityMeasure_iff
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
rw : AEMeasurable (_m := m𝓧) Y (map X P)
⊢ map (Y ∘ X) P = ν

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable _ hX.aemeasurable, hX.map_eq, hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
rw : AEMeasurable Y μ
⊢ AEMeasurable (_m := m𝓧) Y (map X P)

Tactic:
rw [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y μ

Tactic:
hY.aemeasurable

Premises used: ProbabilityTheory.HasLaw.aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y μ

Tactic:
exact hY.aemeasurable

Premises used: ProbabilityTheory.HasLaw.aemeasurable
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ HasLaw (fun (ω : Ω) ↦ Y (X ω)) ν P

Tactic:
hY.comp hX

Premises used: ProbabilityTheory.HasLaw.comp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : MeasurePreserving Y μ ν
hX : HasLaw X μ P
⊢ HasLaw (Y ∘ X) ν P

Tactic:
hY.hasLaw.comp hX

Premises used: MeasureTheory.MeasurePreserving.hasLaw, ProbabilityTheory.HasLaw.comp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : MeasurePreserving Y μ ν
hX : HasLaw X μ P
⊢ HasLaw (fun (ω : Ω) ↦ Y (X ω)) ν P

Tactic:
hY.comp_hasLaw hX

Premises used: MeasureTheory.MeasurePreserving.comp_hasLaw