α : Type u_1
β : Type u_2
γ : Type ?u.67189
ι : Sort ?u.67192
π : α → Type ?u.67197
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
α : Type u_1
β : Type u_2
γ : Type ?u.67189
ι : Sort ?u.67192
π : α → Type ?u.67197
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t
refine' ⟨_, h.rightInvOn_invFunOn⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.67189
ι : Sort ?u.67192
π : α → Type ?u.67197
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
α : Type u_1
β : Type u_2
γ : Type ?u.67189
ι : Sort ?u.67192
π : α → Type ?u.67197
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
rintro _ ⟨y, hy, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.67189
ι : Sort ?u.67192
π : α → Type ?u.67197
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
rw [h.rightInvOn_invFunOn hy]