α : Type u_1
β : Type u_2
γ : Type ?u.112998
ι : Sort ?u.113001
π : α → Type ?u.113006
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.112998
ι : Sort ?u.113001
π : α → Type ?u.113006
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.112998
ι : Sort ?u.113001
π : α → Type ?u.113006
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
exact h.bijOn_image (bijective_iff_bijOn_univ.1 ha) (hf.injOn univ)