[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ condCount ∅ = 0
[PROOFSTEP]
simp [condCount]
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
⊢ ↑↑(condCount s) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
⊢ Set.Finite s
[PROOFSTEP]
by_contra hs'
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
hs' : ¬Set.Finite s
⊢ False
[PROOFSTEP]
simp [condCount, cond, Measure.count_apply_infinite hs'] at h 
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑(condCount Set.univ) s = ↑↑Measure.count s / ↑(Fintype.card Ω)
[PROOFSTEP]
rw [condCount, cond_apply _ MeasurableSet.univ, ← ENNReal.div_eq_inv_mul, Set.univ_inter]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count s / ↑↑Measure.count Set.univ = ↑↑Measure.count s / ↑(Fintype.card Ω)
[PROOFSTEP]
congr
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count Set.univ = ↑(Fintype.card Ω)
[PROOFSTEP]
rw [← Finset.coe_univ, Measure.count_apply, Finset.univ.tsum_subtype' fun _ => (1 : ENNReal)]
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ (Finset.sum Finset.univ fun x => 1) = ↑(Fintype.card Ω)
[PROOFSTEP]
simp [Finset.card_univ]
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ MeasurableSet ↑Finset.univ
[PROOFSTEP]
exact (@Finset.coe_univ Ω _).symm ▸ MeasurableSet.univ
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) Set.univ = 1
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, Set.inter_univ, ENNReal.inv_mul_cancel]
[GOAL]
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0
[PROOFSTEP]
exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
[GOAL]
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 hs).ne
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑(condCount {ω}) t = if ω ∈ t then 1 else 0
[PROOFSTEP]
rw [condCount, cond_apply _ (measurableSet_singleton ω), Measure.count_singleton, inv_one, one_mul]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 1
[PROOFSTEP]
rw [(by simpa : ({ ω } : Set Ω) ∩ t = { ω }), Measure.count_singleton]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ {ω} ∩ t = {ω}
[PROOFSTEP]
simpa
[GOAL]
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 0
[PROOFSTEP]
rw [(by simpa : ({ ω } : Set Ω) ∩ t = ∅), Measure.count_empty]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ {ω} ∩ t = ∅
[PROOFSTEP]
simpa
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (s ∩ t) = ↑↑(condCount s) t
[PROOFSTEP]
rw [condCount, cond_inter_self _ hs.measurableSet]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) s = 1
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
[GOAL]
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0
[PROOFSTEP]
exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
[GOAL]
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 hs).ne
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
⊢ ↑↑(condCount s) t = 1
[PROOFSTEP]
haveI := condCount_isProbabilityMeasure hs hs'
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) t = 1
[PROOFSTEP]
refine' eq_of_le_of_not_lt prob_le_one _
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ¬↑↑(condCount s) t < 1
[PROOFSTEP]
rw [not_lt, ← condCount_self hs hs']
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) s ≤ ↑↑(condCount s) t
[PROOFSTEP]
exact measure_mono ht
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ s ⊆ t
[PROOFSTEP]
have hsf := finite_of_condCount_ne_zero (by rw [h]; exact one_ne_zero)
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ ↑↑(condCount ?m.9273) ?m.9274 ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
hsf : Set.Finite s
⊢ s ⊆ t
[PROOFSTEP]
rw [condCount, cond_apply _ hsf.measurableSet, mul_comm] at h 
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑Measure.count (s ∩ t) * (↑↑Measure.count s)⁻¹ = 1
hsf : Set.Finite s
⊢ s ⊆ t
[PROOFSTEP]
replace h := ENNReal.eq_inv_of_mul_eq_one_left h
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : ↑↑Measure.count (s ∩ t) = (↑↑Measure.count s)⁻¹⁻¹
⊢ s ⊆ t
[PROOFSTEP]
rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _), Nat.cast_inj] at h 
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ⊆ t
[PROOFSTEP]
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
this : s ∩ t = s
⊢ s ⊆ t
[PROOFSTEP]
exact this ▸ fun x hx => hx.2
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ∩ t = s
[PROOFSTEP]
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ Set.Finite.toFinset (_ : Set.Finite (s ∩ t)) = Set.Finite.toFinset hsf
[PROOFSTEP]
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono <| s.inter_subset_left t) h.ge
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) t = 0 ↔ s ∩ t = ∅
[PROOFSTEP]
simp [condCount, cond_apply _ hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
  Measure.count_apply_finite _ (hs.inter_of_left _)]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
by_cases hst : s ∩ t = ∅
[GOAL]
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
rw [hst, condCount_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul, condCount_eq_zero_iff hs, ← Set.inter_assoc,
  hst, Set.empty_inter]
[GOAL]
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
rw [condCount, condCount, 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]
[GOAL]
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ 0
[PROOFSTEP]
rwa [← Measure.count_eq_zero_iff] at hst 
[GOAL]
case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u
[PROOFSTEP]
rw [← Set.inter_comm]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (u ∩ t) = ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u
[PROOFSTEP]
exact condCount_inter hs
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ ↑↑(condCount s) (t ∪ u) = ↑↑(condCount s) t + ↑↑(condCount s) u
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet,
  Set.inter_union_distrib_left, measure_union, mul_add]
[GOAL]
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)
case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)
[PROOFSTEP]
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u t : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) t + ↑↑(condCount s) tᶜ = 1
[PROOFSTEP]
rw [← condCount_union hs disjoint_compl_right, Set.union_compl_self,
  (condCount_isProbabilityMeasure hs hs').measure_univ]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs')
[GOAL]
case inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : Set.Finite t
hs : Set.Finite ∅
hst : Disjoint ∅ t
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ t)) ∅ + ↑↑(condCount t) u * ↑↑(condCount (∅ ∪ t)) t = ↑↑(condCount (∅ ∪ t)) u
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht')
[GOAL]
case inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht')
[GOAL]
case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : Set.Finite ∅
hst : Disjoint ∅ ∅
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ ∅)) ∅ + ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ ∅)) ∅ = ↑↑(condCount (∅ ∪ ∅)) u
[PROOFSTEP]
simp
[GOAL]
case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : Set.Finite t
hs : Set.Finite ∅
hst : Disjoint ∅ t
ht' : Set.Nonempty t
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ t)) ∅ + ↑↑(condCount t) u * ↑↑(condCount (∅ ∪ t)) t = ↑↑(condCount (∅ ∪ t)) u
[PROOFSTEP]
simp [condCount_self ht ht']
[GOAL]
case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : Set.Finite ∅
hst : Disjoint s ∅
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ ∅)) s + ↑↑(condCount ∅) u * ↑↑(condCount (s ∪ ∅)) ∅ = ↑↑(condCount (s ∪ ∅)) u
[PROOFSTEP]
simp [condCount_self hs hs']
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rw [condCount, condCount, condCount, 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]
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ (↑↑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)
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑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))
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑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))
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑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))
[PROOFSTEP]
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]
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑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)
[PROOFSTEP]
rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
  Set.union_inter_distrib_right, mul_comm]
[GOAL]
case inr.inr.hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ Disjoint (s ∩ u) (t ∩ u)
case inr.inr.h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ MeasurableSet (t ∩ u)
case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count t ≠ 0
case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count t ≠ ⊤
case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count s ≠ 0
case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ = ↑↑(condCount s) t
[PROOFSTEP]
have :
  condCount s t =
    (condCount (s ∩ u) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ u) +
      condCount (s ∩ uᶜ) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ uᶜ)) :=
  by
  rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right),
    Set.inter_union_compl]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
[PROOFSTEP]
rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
    (disjoint_compl_right.mono inf_le_right inf_le_right),
  Set.inter_union_compl]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ = ↑↑(condCount s) t
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
[PROOFSTEP]
simp [condCount_inter_self hs]
