α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift (#↑s) ≤ lift (#↑(f ⁻¹' s))
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ (#↑s) ≤ (#↑(f ⁻¹' s))
rw [← lift_id (#↑(f ⁻¹' s)), ← lift_id (#↑(s))]
no goals
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift (#↑s) ≤ lift (#↑(f ⁻¹' s))
exact mk_preimage_of_subset_range_lift f s h