ProbabilityTheory.IndepFun.comp_right

lemma IndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)    (hf : Measurable f) (hg : Measurable g) (hfg : IndepFun f g μ) :    IndepFun (f ∘ i) (g ∘ i) (μ.comap i) := by  change μ (range i)ᶜ = 0 at hi'  rw [IndepFun_iff] at hfg ⊢  rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩  rw [preimage_comp, preimage_comp, ← preimage_inter, comap_apply, comap_apply, comap_apply,    image_preimage_eq_inter_range, image_preimage_eq_inter_range, image_preimage_eq_inter_range,    measure_inter_conull hi', measure_inter_conull hi', measure_inter_conull hi',    hfg _ _ ⟨_, hs, rfl⟩ ⟨_, ht, rfl⟩]  all_goals first  | exact hi.injective  | exact hi.measurableSet_image'  | exact hi.measurable <| hf hs  | exact hi.measurable <| hg ht  | exact hi.measurable <| (hf hs).inter <| hg ht