awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have pos₂ : ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
  HMul.hMul (α := ENNReal) (β := ENNReal) (0 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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have pos₃ : ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
  HMul.hMul (α := ENNReal) (β := ENNReal) (0 : 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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have pos₄ : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal) (0 : 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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have pos₅ : s ∩ (t ∩ u) = ∅
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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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) = ∅
⊢ ((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)
have pos₆ : s ∩ t ∩ u = ∅
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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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 = ∅
⊢ ((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)
have pos₇ : ∅ ∩ u = ∅
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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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 = ∅
⊢ ((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)
have pos₈ : Eq.{u_1 + 1} (α := Set Ω) ∅ ∅
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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
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)
have neg : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (0 : 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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have neg₁ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal) (⊤ : 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]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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) (0 : ENNReal)
have 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)
Tactic: rwa [← Measure.count_eq_zero_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ ((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)
have 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)
Tactic: rw [← Set.inter_comm]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t 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)
have hd : Disjoint (s ∩ t) (s ∩ u)
Tactic: rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ ((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)
have h : MeasurableSet (s ∩ u)
Tactic: rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) tᶜ : ENNReal) =
    1
have rw : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∪ tᶜ) : ENNReal) (1 : ENNReal)
Tactic: rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (isProbabilityMeasure_uniformOn hs hs').measure_univ]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) tᶜ : ENNReal) =
    1
have rw₁ : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) Set.univ : ENNReal) (1 : ENNReal)
Tactic: rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (isProbabilityMeasure_uniformOn hs hs').measure_univ]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) tᶜ : ENNReal) =
    1
have rw₂ : Eq (α := ENNReal) 1 1
Tactic: rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (isProbabilityMeasure_uniformOn hs hs').measure_univ]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
⊢ 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
have 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
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs')
Cleared hypotheses: s, hs, hst
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
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
⊢ 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
have 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
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs')
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
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
have 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
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht')
Cleared hypotheses: t, ht, hst