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