no goals
α : Type u_1
β : Type u_2
ι : Type ?u.1452280
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ↑↑(↑(comapRight κ hf) a) t = ↑↑(↑κ a) (f '' t)
rw [comapRight_apply,
  Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]