no goals
α : Type u_1
β : Type u_2
γ : Type ?u.101627
ι : Sort ?u.101630
π : α → Type ?u.101635
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (restrict s f) ↔ StrictMonoOn f s
simp [Set.restrict, StrictMono, StrictMonoOn]