no goals
α : Type u_1
β : Type ?u.589734
γ : Type ?u.589737
δ : Type ?u.589740
ι : Type ?u.589743
R : Type ?u.589746
R' : Type ?u.589749
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s t : α → Prop
hst : s =ᶠ[ae μ] t
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ s, p x) → ∀ᵐ (x : α) ∂Measure.restrict μ t, p x
simp [Measure.restrict_congr_set hst]