∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α}
  {f g : α → γ}, AEMeasurable f μ → f =ᵐ[μ] g → ProbabilityTheory.IdentDistrib f g μ μ