Lean4
/-- It suffices to prove `f` is monotone between strict relations
to show it is a relation embedding. -/
def ofMonotone [IsTrichotomous α r] [IsAsymm β s] (f : α → β) (H : ∀ a b, r a b → s (f a) (f b)) : r ↪r s :=
by
haveI := @IsAsymm.isIrrefl β s _
refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
· refine ((@trichotomous _ r _ a b).resolve_left ?_).resolve_right ?_
· exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)
· exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)
· refine (@trichotomous _ r _ a b).resolve_right (Or.rec (fun e => ?_) fun h' => ?_)
· subst e
exact irrefl _ h
· exact asymm (H _ _ h') h
