ι : Type ?u.27119
α : Type u
β : Type v
γ : Type w
δ : Type ?u.27128
π : ι → Type ?u.27133
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
ι : Type ?u.27119
α : Type u
β : Type v
γ : Type w
δ : Type ?u.27128
π : ι → Type ?u.27133
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b
rintro rfl
no goals
ι : Type ?u.27119
α : Type u
β : Type v
γ : Type w
δ : Type ?u.27128
π : ι → Type ?u.27133
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
rfl