preorder.lift'

Stream: general

[Johan Commelin]

How do people feel about adding

/-- version of preorder.lift which doesn't use type class inference -/
def lift' : preorder β → (α → β) → preorder α := @preorder.lift _ _

to mathlib? We use it twice in the perfectoid project. But we can of course also use @preorder.lift _ _ .
(And yes, we are quite sure we don't want to use type class instances for these preorders, because we are looking at something like the type of all preorders on a ring that satisfy blah...)

If we add this to mathlib, I guess we also want partial_order.lift' etc, etc...

[Mario Carneiro]

I think you can just replace preorder.lift with this. It's usually used to create instances, so having a by apply_instance in there doesn't seem so bad

[Mario Carneiro]

I would put the preorder argument second though

[Johan Commelin]

Probably breaks a lot of files... and I don't have VScode atm (-; But let me see what I can do...

[Johan Commelin]

#995 -- let's see what Travis says. This PR was produced using grep and vim, without running Lean...

[Johan Commelin]

And... I failed. Travis doesn't like it

[Johan Commelin]

Hurray, after several iterations #995 passes the checks on Travis. (And I never ran Lean locally :grimacing:)