case hs
ι : Sort ?u.104761
α : Type u_2
β : Type u_1
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
ι : Sort ?u.104761
α : Type u_2
β : Type u_1
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
apply Set.preimage_subset_preimage_iff
case hs
ι : Sort ?u.104761
α : Type u_2
β : Type u_1
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ
case hs
ι : Sort ?u.104761
α : Type u_2
β : Type u_1
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
rw [Function.Surjective.range_eq hf]
no goals
case hs
ι : Sort ?u.104761
α : Type u_2
β : Type u_1
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ
apply subset_univ