Trouble with composition of maps for a functor over a preord

Stream: new members

[Rémi Bottinelli]

I'm not sure how to describe my problem. I'm trying to construct, given an inverse system of types, the subsystem consisting of the "surjective" parts here and I'm having trouble showing what should be obvious, or so I thought. What am I doing wrong here?
To be a bit more precise, at some point I have the goal

F.map (op_hom_of_le _) (F.map (op_hom_of_le lk) y) = F.map (op_hom_of_le kj) (F.map (op_hom_of_le lk) y)

where I would swear the _ should be a shorthand for op_hom_of_le kj, thus making the goal trivial. I can't pinpoint the reason it isn't the case, and I didn't figure out how to ask lean to tell me what exactly should be at the _.
Ah, I might as well paste the whole goal context:

J : Type u,
_inst_1 : preorder J,
_inst_2 : is_directed J has_le.le,
F : Jᵒᵖ ⥤ Type v,
bigger : Jᵒᵖ → set Jᵒᵖ := λ (j : Jᵒᵖ), {i : Jᵒᵖ | opposite.unop j ≤ opposite.unop i},
Fsur_obj : Π (j : Jᵒᵖ), set (F.obj j) :=
  λ (j : Jᵒᵖ), ⋂ (i : ↥(bigger j)), set.range (F.map (op_hom_of_le _)),
i j : Jᵒᵖ,
hij : i ⟶ j,
k : Jᵒᵖ,
kj : k ∈ bigger j,
kj : opposite.unop j ≤ opposite.unop k,
l' : J,
lk' : opposite.unop k ≤ l',
li' : opposite.unop i ≤ l',
l : Jᵒᵖ := opposite.op l',
lk : opposite.unop k ≤ opposite.unop l,
li : opposite.unop i ≤ opposite.unop l,
hlk : l ⟶ k := op_hom_of_le lk,
hli : l ⟶ i := op_hom_of_le li,
hkj : k ⟶ j := op_hom_of_le kj,
y : F.obj ↑⟨l, li⟩,
h : ∀ (i_1 : ↥(bigger i)), ∃ (y_1 : F.obj ↑i_1), F.map (op_hom_of_le _) y_1 = F.map (op_hom_of_le _) y
⊢ F.map (op_hom_of_le _) (F.map (op_hom_of_le lk) y) = F.map (op_hom_of_le kj) (F.map (op_hom_of_le lk) y)

[Andrew Yang]

rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply],
refl

solves the particular goal you described.

[Andrew Yang]

Or even a single refl suffices if I am not mistaken.

[Rémi Bottinelli]

Huh, it's very confusing, I tried things very close to that. So my intuition was correct? that is, the underscore really was op_hom_of_le kj?

[Andrew Yang]

You can click on the _ in the info view to see the hidden term. In this case it is subtype.prop ⟨k, kj⟩ which is definitionally equal to kj, but not syntactically equal, so dsimp did not close the goal for you.

In fact, due to proof irrelavence, two Props are defeq whenever they have the same type, so it doesn't even matter what the term is (and hence it is hidden in the infoview).

[Rémi Bottinelli]

OK, that does match my intuition, thanks a lot! So, what I did wrong was essentially to not try for refl early enough, since I _did_ have defeq terms?

[Andrew Yang]

Probably yes. It never hurts to try refl.
This is how I would approach subfunctor:

{ rintro i j hij,
    rintro x h s ⟨⟨k, _⟩, rfl⟩,
    obtain ⟨l,lk,li⟩ := directed_of (≤) k.unop i.unop,
    rw set.mem_Inter at h,
    obtain ⟨y,rfl⟩ := h ⟨opposite.op l, li⟩,
    use F.map (hom_of_le lk).op y,
    rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply],
    refl },

[Rémi Bottinelli]

I'm also wondering: The following doesn't typecheck. That's because of the lifting involved in the instantiation of J as a category, am I right?

example {J : Type u} [preorder J] (i j : Jᵒᵖ) (m n : i ⟶ j) : m = n, by reflexivity

And the following does typecheck:

example {J : Type u} [preorder J] (i j : Jᵒᵖ) (m n : i ⟶ j) : m ≫ (𝟙 j) = n ≫ (𝟙 j) := rfl

becauses it forces the passage through a Prop. That's fun