Cannot get lean to see I have declared an instance

Stream: new members

[Will Fourie]

Hello, I am having an issue at the moment where I am struggling to get lean to recognise that I have (started) to define a particular category.

I am trying to define the category attached to any reflexive transitive relation, and have introduced variables for the relation and defined the category using those variables, however whenever I try to use that definition, lean pretends it doesn't see it.

I am not exactly sure what I am doing wrong here?

  universes u
  class rel_cat_data (T : Type u) :=  (rel : T→ T→ Prop) (rel_refl : reflexive rel) (rel_trans : transitive rel)
  variables {S: Type u} [rel_cat_data S]
  open rel_cat_data

  local notation a ~ b := rel a b

  instance rel_cat  : category S :=
  {
    hom := λ(a b : S), ulift( plift (rel a b)),
    id := λ(a:S), ulift.up (plift.up (rel_refl a)),
    comp := λ a b c r1 r2, by
    {
      let r1' := plift.down (ulift.down r1),
      let r2' := plift.down (ulift.down r2),
      let r3' := rel_trans r1' r2',
      exact ulift.up (plift.up r3'),
    }

  }

--this does not work for some reason
  lemma test1 (a b : S) : (a ⟶ b) = (λ(a b : S), ulift ( plift (rel a b))) a b := sorry
  /-
  failed to synthesize type class instance for
  S : Type u,
  _inst_3 : rel_cat_data S,
  a b : S
  ⊢ quiver S
  -/

  --and yet this works ???
  lemma test2 (a b : S) : (rel_cat.hom a b) = (λ(a b : S), ulift ( plift (rel a b))) a b :=
  begin
    refl,
  end

[Kevin Buzzard]

Can you post a #mwe ? This code doesn't compile as it stands.