no goals
α : Type u_1
β : Type u_2
ι : Type ?u.361579
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → ↑↑(↑κ a) s = ↑↑(↑η a) s
simp_rw [ext_iff, Measure.ext_iff]