α : Type u_1
β : Type u_2
γ : Type ?u.111695
ι : Sort ?u.111698
π : α → Type ?u.111703
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.111695
ι : Sort ?u.111698
π : α → Type ?u.111703
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.111695
ι : Sort ?u.111698
π : α → Type ?u.111703
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
exact h.surjOn_image (ha.surjOn univ)