ProbabilityTheory.IndepFun.cond

lemma IndepFun.cond (hi : IndepFun A B μ) {s : Set α} {t : Set β}    (hs : MeasurableSet s) (ht : MeasurableSet t) (hA : Measurable A) (hB : Measurable B) :    IndepFun A B (μ[| A ⁻¹' s ∩ B ⁻¹' t]) := by  apply indepFun_iff_measure_inter_preimage_eq_mul.2 (fun u v hu hv ↦ ?_)  have I1 : A ⁻¹' s ∩ B ⁻¹' t ∩ (A ⁻¹' u ∩ B ⁻¹' v) = A ⁻¹' (s ∩ u) ∩ B ⁻¹' (t ∩ v) := by aesop  have I2 : A ⁻¹' s ∩ B ⁻¹' t ∩ A ⁻¹' u = A ⁻¹' (s ∩ u) ∩ B ⁻¹' t := by aesop  have I3 : A ⁻¹' s ∩ B ⁻¹' t ∩ B ⁻¹' v = A ⁻¹' s ∩ B ⁻¹' (t ∩ v) := by aesop  simp only [cond_apply ((hA hs).inter (hB ht)), I1, I2, I3]  rcases eq_or_ne (μ (A ⁻¹' s ∩ B⁻¹' t)) ∞ with h|h  · simp [h]  rcases eq_or_ne (μ (A ⁻¹' s ∩ B⁻¹' t)) 0 with h'|h'  · have I : μ (A ⁻¹' (s ∩ u) ∩ B ⁻¹' (t ∩ v)) = 0 := by      apply le_antisymm ((measure_mono _).trans h'.le) bot_le      exact inter_subset_inter (preimage_mono inter_subset_left)        (preimage_mono inter_subset_left)    have J : μ (A ⁻¹' (s ∩ u) ∩ B ⁻¹' t) = 0 := by      apply le_antisymm ((measure_mono _).trans h'.le) bot_le      exact inter_subset_inter_left _ (preimage_mono inter_subset_left)    simp only [I, J, mul_zero, zero_mul]  · simp only [hi.measure_inter_preimage_eq_mul _ _ hs ht, ne_eq, mul_eq_zero, not_or] at h'    simp only [hi.measure_inter_preimage_eq_mul _ _ hs ht, ne_eq, ENNReal.mul_eq_top, h'.1,      not_false_eq_true, true_and, h'.2, and_true, not_or] at h    rw [mul_assoc]    congr 1    rw [hi.measure_inter_preimage_eq_mul _ _ (hs.inter hu) (ht.inter hv),      hi.measure_inter_preimage_eq_mul _ _ (hs.inter hu) ht,      hi.measure_inter_preimage_eq_mul _ _ hs ht,      hi.measure_inter_preimage_eq_mul _ _ hs (ht.inter hv),      ENNReal.mul_inv (Or.inl h'.1) (Or.inr h'.2), mul_assoc]    congr 1    have : μ (B ⁻¹' t) * ((μ (A ⁻¹' s))⁻¹ * (μ (B ⁻¹' t))⁻¹ * (μ (A ⁻¹' s) * μ (B ⁻¹' (t ∩ v))))      = (μ (B ⁻¹' t) * (μ (B ⁻¹' t))⁻¹) * ((μ (A ⁻¹' s))⁻¹ * μ (A ⁻¹' s)) * μ (B ⁻¹' (t ∩ v)) := by        ring    rw [this, ENNReal.inv_mul_cancel h'.1 h.2, ENNReal.mul_inv_cancel h'.2 h.1, one_mul, one_mul]