Opposite order `nonempty_sections_of_fintype_inverse_system`

Stream: new members

[Junyan Xu]

@Rémi Bottinelli It's easier to derive the desired result from docs#nonempty_sections_of_fintype_cofiltered_system by mimicking the proof of src#nonempty_sections_of_fintype_inverse_system:

import topology.category.Top.limits

universes u v

variables {J : Type u} [preorder J] [is_directed J ge] (F : J ⥤ Type v)

theorem nonempty_sections_of_fintype_inverse_system'
 [fin : Π (j : J), fintype (F.obj j)] [nempty : ∀ (j : J), nonempty (F.obj j)] : F.sections.nonempty :=
begin
  casesI is_empty_or_nonempty J,
  { exact ⟨is_empty_elim, is_empty_elim⟩, },
  { exact nonempty_sections_of_fintype_cofiltered_system _, },
end

[Junyan Xu]

I think the error you get is due to the category structure you get from
Joppreo : preorder Jᵒᵖ ⟿ category Jᵒᵖ is different from
preorder J ⟿ category J ⟿ category Jᵒᵖ,
which is known as a diamond.
(normally you would get the opposite preorder using docs#order_dual Jᵒᵈ instead of Jᵒᵖ, but then you won't be able to use category_theory.op_op.)