α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.58114
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ↑f ⁻¹' s = ↑f ⁻¹' (g ⁻¹' s)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.58114
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ ↑(map g f) ⁻¹' s = ↑f ⁻¹' ↑(Finset.filter (fun b => g b ∈ s) (SimpleFunc.range f))
simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter,
  ← mem_preimage, inter_comm, preimage_inter_range, ← Finset.mem_coe]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.58114
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ↑f ⁻¹' s = ↑f ⁻¹' (g ⁻¹' s)
exact preimage_comp