no goals
α : Type u_2
β✝ : Type ?u.120092
R : Type ?u.120095
R' : Type ?u.120098
ms : Set (OuterMeasure α)
m : OuterMeasure α
β : Type u_1
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : ↑(map f) ma ≤ mb
s : Set β
⊢ ↑(↑(map f) ma) s ≤ ↑(↑(restrict (range f)) mb) s
simpa using h (s ∩ range f)