no goals
α : Type u_1
β : Type ?u.901885
γ : Type ?u.901888
δ : Type ?u.901891
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
h : ↑f =ᵐ[μ] ↑g
y : ℝ≥0∞
x : α
hx : ↑f x = ↑g x
⊢ x ∈ ↑f ⁻¹' {y} ↔ x ∈ ↑g ⁻¹' {y}
simp [hx]