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 Ω
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
⊢ 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' : 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: rcases t.eq_empty_or_nonempty with (rfl | ht')
-- 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
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
have 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
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht')
Cleared hypotheses: t, ht, 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
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
⊢ 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₁ : ∀ (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
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht')
-- 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
hs' : s.Nonempty
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
have 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)
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]
-- 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
hs' : s.Nonempty
ht' : t.Nonempty
| 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)
have rw : HMul.hMul (β := ENNReal)
    (HMul.hMul (β := ENNReal)
      (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
    ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
  HMul.hMul (β := ENNReal)
    (HMul.hMul (β := ENNReal)
      (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
    ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
Tactic: rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ 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)
have inr : HMul.hMul (β := ENNReal)
      (HMul.hMul (β := ENNReal)
        (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
    HMul.hMul (β := ENNReal)
      (HMul.hMul (β := ENNReal)
        (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
Tactic: conv_lhs =>
    rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr : Disjoint (s ∩ u) (t ∩ u)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr₁ : MeasurableSet (t ∩ u)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
inr₁ : MeasurableSet (t ∩ u)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr₂ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
inr₁ : MeasurableSet (t ∩ u)
inr₂ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr₃ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (⊤ : ENNReal)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
inr₁ : MeasurableSet (t ∩ u)
inr₂ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
inr₃ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (⊤ : ENNReal)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr₄ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
inr₁ : MeasurableSet (t ∩ u)
inr₂ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
inr₃ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (⊤ : ENNReal)
inr₄ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ 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)
have inr₅ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
Tactic: rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
| ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t
have rw : HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
    (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) +
  HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
    (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ uᶜ) : ENNReal)
Tactic: rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ),
      ← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal) +
      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
have conv_rhs : HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal) +
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) uᶜ : ENNReal) =
  HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) +
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ uᶜ) : ENNReal)
Tactic: conv_rhs =>
    rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ),
      ← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)]