α : Type u_1
β : Type u_2
γ : Type ?u.67762
ι : Sort ?u.67765
π : α → Type ?u.67770
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t
α : Type u_1
β : Type u_2
γ : Type ?u.67762
ι : Sort ?u.67765
π : α → Type ?u.67770
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t
refine' h.invOn_invFunOn.bijOn _ (mapsTo_image _ _)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.67762
ι : Sort ?u.67765
π : α → Type ?u.67770
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t
α : Type u_1
β : Type u_2
γ : Type ?u.67762
ι : Sort ?u.67765
π : α → Type ?u.67770
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t
rintro _ ⟨y, hy, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.67762
ι : Sort ?u.67765
π : α → Type ?u.67770
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t
rwa [h.rightInvOn_invFunOn hy]