ProbabilityTheory.IndepFun.cond_left

lemma IndepFun.cond_left (hi : IndepFun A B μ) {s : Set α}    (hs : MeasurableSet s) (hA : Measurable A) :    IndepFun A B (μ[| A⁻¹' s]) := by  apply indepFun_iff_measure_inter_preimage_eq_mul.2 (fun u v hu hv ↦ ?_)  have : A ⁻¹' s ∩ (A ⁻¹' u ∩ B ⁻¹' v) = A ⁻¹' (s ∩ u) ∩ B ⁻¹' v := by aesop  simp only [cond_apply (hA hs), this]  rcases eq_or_ne (μ (A ⁻¹' s)) ∞ with h|h  · simp [h]  rcases eq_or_ne (μ (A ⁻¹' s)) 0 with h'|h'  · have I : μ (A ⁻¹' (s ∩ u) ∩ B ⁻¹' v) = 0 := by      apply le_antisymm ((measure_mono _).trans h'.le) bot_le      exact inter_subset_left.trans (preimage_mono inter_subset_left)    have J : μ (A ⁻¹' s ∩ B ⁻¹' v) = 0 :=      le_antisymm ((measure_mono inter_subset_left).trans h'.le) bot_le    simp only [I, J, mul_zero]  · rw [hi.measure_inter_preimage_eq_mul _ _ (hs.inter hu) hv, Set.preimage_inter,      hi.measure_inter_preimage_eq_mul _ _ hs hv, ← mul_assoc (μ (A ⁻¹' s))⁻¹,      ← mul_assoc (μ (A ⁻¹' s))⁻¹, ENNReal.inv_mul_cancel h' h, one_mul]