awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
this : s ∩ t = s
⊢ s ⊆ t

Tactic:
this ▸ fun x hx => hx.2

Premises used: Eq.rec, And.right
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
this : s ∩ t = s
⊢ s ⊆ t

Tactic:
exact this ▸ fun x hx => hx.2
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
suffices : s ∩ t = s
⊢ s ⊆ t

Tactic:
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
rw : ⋯.toFinset (s := s ∩ t) = hsf.toFinset (s := s)
⊢ s ∩ t = s

Tactic:
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]

Premises used: Set.Finite.toFinset_inj
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
⊢ ⋯.toFinset (s := s ∩ t) = hsf.toFinset (s := s)

Tactic:
Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge

Premises used: Eq.ge, Set.inter_subset_left, Set.Finite.toFinset_mono, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
⊢ ⋯.toFinset (s := s ∩ t) = hsf.toFinset (s := s)

Tactic:
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge

Premises used: Eq.ge, Set.inter_subset_left, Set.Finite.toFinset_mono, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal) ↔ s ∩ t = ∅

Tactic:
simp [uniformOn, cond_apply hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
    Measure.count_apply_finite _ (hs.inter_of_left _)]

Premises used: Iff.mpr, ProbabilityTheory.cond_apply, Set.Finite.inter_of_left, MeasureTheory.Measure.count_apply_eq_top, Set.not_infinite, MeasureTheory.Measure.count_apply_finite, Set.Finite.measurableSet, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) Set.univ : ENNReal) (1 : ENNReal)

Tactic:
uniformOn_eq_one_of hs hs' s.subset_univ

Premises used: Set.subset_univ, ProbabilityTheory.uniformOn_eq_one_of
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
pos :
  ∀ (hst : s ∩ t = ∅),
    ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
neg :
  ∀ (hst : ¬s ∩ t = ∅),
    ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
by_cases hst : s ∩ t = ∅
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
pos :
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
pos₁ :
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((0 : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
pos₂ :
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (0 u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
pos₃ :
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
pos₄ : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal) (0 : ENNReal)
pos₅ : s ∩ (t ∩ u) = ∅
pos₆ : s ∩ t ∩ u = ∅
pos₇ : ∅ ∩ u = ∅
pos₈ pos₉ : Eq.{u_1 + 1} (α := Set Ω) ∅ ∅
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
rw [hst, uniformOn_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul,
      uniformOn_eq_zero_iff hs, ← Set.inter_assoc, hst, Set.empty_inter]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Set.empty_inter, ProbabilityTheory.uniformOn_empty_meas, ProbabilityTheory.uniformOn_eq_zero_iff, Set.inter_assoc, MeasureTheory.Measure.coe_zero
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
neg : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
neg₁ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (⊤ : ENNReal)
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
rw [uniformOn, uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)),
    ← mul_assoc, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul,
    mul_comm, Set.inter_assoc]

Premises used: ProbabilityTheory.cond_apply, Set.Finite.inter_of_left, mul_assoc, Inter.inter, ENNReal.mul_inv_cancel, mul_comm, MeasureTheory.Measure.count, DFunLike.coe, Set.Finite.measurableSet, Set.inter_assoc, ProbabilityTheory.uniformOn, one_mul
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
neg neg₁ neg₂ neg₃ :
  ∀ (hst : ¬Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)),
    Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)

Tactic:
rwa [← Measure.count_eq_zero_iff] at hst

Premises used: MeasureTheory.Measure.count_eq_zero_iff
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (⊤ : ENNReal)

Tactic:
(Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne

Premises used: Iff.mpr, Set.Finite.inter_of_left, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (⊤ : ENNReal)

Tactic:
exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne

Premises used: Iff.mpr, Set.Finite.inter_of_left, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
rw :
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (u ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)

Tactic:
rw [← Set.inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (u ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)

Tactic:
uniformOn_inter hs

Premises used: ProbabilityTheory.uniformOn_inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (u ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)

Tactic:
exact uniformOn_inter hs

Premises used: ProbabilityTheory.uniformOn_inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
hd : Disjoint (s ∩ t) (s ∩ u)
h : MeasurableSet (s ∩ u)
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∪ u) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)

Tactic:
rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]

Premises used: ProbabilityTheory.cond_apply, MeasureTheory.measure_union, mul_add, Set.Finite.measurableSet, Set.inter_union_distrib_left, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

Tactic:
htu.mono inf_le_right inf_le_right

Premises used: inf_le_right, Disjoint.mono
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)

Tactic:
(hs.inter_of_left _).measurableSet

Premises used: Set.Finite.inter_of_left, Set.Finite.measurableSet
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

Tactic:
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]

Premises used: Set.Finite.inter_of_left, inf_le_right, Disjoint.mono, Set.Finite.measurableSet
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
rw : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∪ tᶜ) : ENNReal) (1 : ENNReal)
rw₁ : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) Set.univ : ENNReal) (1 : ENNReal)
rw₂ rw₃ : Eq (α := ENNReal) 1 1
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) tᶜ : ENNReal) =
    1

Tactic:
rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (isProbabilityMeasure_uniformOn hs hs').measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, Set.union_compl_self, ProbabilityTheory.uniformOn_union, disjoint_compl_right
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
inl :
  ∀ (hs : Set.Finite.{u_1} (α := Ω) ∅) (hst : Disjoint ∅ t),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
      ((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u
inr :
  ∀ (hs' : s.Nonempty),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
      ((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
    ((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs')

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : Set.Finite.{u_1} (α := Ω) ∅
hst : Disjoint ∅ t
inl :
  ∀ (ht : Set.Finite.{u_1} (α := Ω) ∅) (hst : Disjoint.{u_1} (α := Set Ω) ∅ ∅),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) =
      ((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) u
inl₁ :
  ∀ (ht' : t.Nonempty),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
      ((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
    ((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht')

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
inr :
  ∀ (ht : Set.Finite.{u_1} (α := Ω) ∅) (hst : Disjoint s ∅),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) =
      ((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) u
inr₁ :
  ∀ (ht' : t.Nonempty),
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
        HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
          (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
      ((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
    ((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht')

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
u : Set Ω
hs ht : Set.Finite.{u_1} (α := Ω) ∅
hst : Disjoint.{u_1} (α := Set Ω) ∅ ∅
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) =
    ((uniformOn (∅ ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
simp
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : Set.Finite.{u_1} (α := Ω) ∅
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
    ((uniformOn (∅ ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
simp [uniformOn_self ht ht']

Premises used: ProbabilityTheory.uniformOn_self
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : Set.Finite.{u_1} (α := Ω) ∅
hst : Disjoint s ∅
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) =
    ((uniformOn (s ∪ ∅) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
simp [uniformOn_self hs hs']

Premises used: ProbabilityTheory.uniformOn_self
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) *
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ s) : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal) *
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ u) : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn t : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) =
    ((uniformOn (s ∪ t) : Measure Ω) : (a : Set Ω) → ENNReal) u

Tactic:
rw [uniformOn, uniformOn, uniformOn, cond_apply hs.measurableSet,
    cond_apply ht.measurableSet, cond_apply (hs.union ht).measurableSet,
    cond_apply (hs.union ht).measurableSet, cond_apply (hs.union ht).measurableSet]

Premises used: Set.Finite.union, ProbabilityTheory.cond_apply, Set.Finite.measurableSet, ProbabilityTheory.uniformOn