-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_disjoint_union (hs : s.Finite) (ht : t.Finite) (hst : Disjoint s t) :
    uniformOn s u * uniformOn (s ∪ t) s + uniformOn t u * uniformOn (s ∪ t) t =
      uniformOn (s ∪ t) u

Proof state:
case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

Tactic:
simp [uniformOn_self ht ht']

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs') <;> rcases t.eq_empty_or_nonempty with (rfl | ht')

Result:
case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : ∅.Finite
hst : Disjoint ∅ ∅
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ + (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ = (uniformOn (∅ ∪ ∅)) u

case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Proof state:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
      Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹ =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ 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]

Result:
case inr.inr.hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Disjoint (s ∩ u) (t ∩ u)

case inr.inr.h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ MeasurableSet (t ∩ u)

case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count t ≠ 0

case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count t ≠ ⊤

case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s ≠ 0

case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s ≠ ⊤

Proof state:
case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : ∅.Finite
hst : Disjoint ∅ ∅
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ + (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ = (uniformOn (∅ ∪ ∅)) u

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Disjoint (s ∩ u) (t ∩ u)

case inr.inr.h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ MeasurableSet (t ∩ u)

case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count t ≠ 0

case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count t ≠ ⊤

case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s ≠ 0

case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s ≠ ⊤

Tactic:
exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet,
  Measure.count_ne_zero ht', (Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs',
  (Measure.count_apply_lt_top.2 hs).ne]

Result:
no goals

Proof state:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) 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]

Result:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)

Proof state:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)

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]

Result:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
      Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹ =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)