Trouble with order_hom_class needing implicit parameters

Stream: general

[Peter Nelson]

I'm trying to define preimages of upper sets under order homs/embeddings/isos, and it seemed to me that order_hom_classwas the right abstraction to do this. The definition I need works, but it seems that I can't actually use it without ugly @ + _ _ _ _ . MWE is below - is there a way around this?

import order.upper_lower

variables {α β F : Type*} [preorder α] [preorder β] [order_hom_class F α β]

/-- The preimage of an `upper_set` under an `order_hom`-like function, as an `upper_set` -/
def upper_set.comap (t : upper_set β) (φ : F) : upper_set α := ⟨φ ⁻¹' t, sorry⟩
-- the sorry replaces a proof that the preimage is an upper_set


example (t : upper_set β) (φ : α →o β):
  @upper_set.comap α β _ _ _ _ t φ  = @upper_set.comap α β _ _ _ _ t φ := rfl
-- works fine

example (t : upper_set β) (φ : α →o β) : t.comap φ = t.comap φ
-- Won't parse t.comap φ
-- failed to synthesize type class instance for
-- α : Type u_1,
-- β : Type u_2,
-- _inst_1 : preorder α,
-- _inst_2 : preorder β,
-- t : upper_set β,
-- φ : α →o β
-- ⊢ order_hom_class (α →o β) ?m_1 β

[Eric Rodriguez]

docs#order_hom_class

[Eric Rodriguez]

I feel like this is the sort of problem out_param should solve but for some reason it seems to not...

[Eric Rodriguez]

(e.g. example (t : upper_set β) (φ : α →o β) (x : upper_set α) : x = t.comap φ := sorry works)

[Eric Rodriguez]

if you annotate the lhs with the right type stuff should work though

[Peter Nelson]

Eric Rodriguez said:

if you annotate the lhs with the right type stuff should work though

edit: nvm, thanks!

[Eric Rodriguez]

you only need to do the lhs, fwiw, as eq requires equal types on both sides