Help with a proof about elements of a functor as pullback

Stream: new members

[Slavomir Kaslev]

I'm trying to prove that any functor F : C ⥤ Type u has pullback along the functor CategoryOfElements.π (𝟭 (Type u)) but got stuck on why the rw below doesn't work

import Mathlib.CategoryTheory.Elements
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

open CategoryTheory Equiv Limits

universe u

abbrev U := Type u
abbrev U' : U := (𝟭 U).Elements
abbrev pᵤ : U' ⥤ U := CategoryOfElements.π (𝟭 U)
def U'_spec : U' = Σ c : U, c := rfl

section
variable {C : U} [Category C] (F : C ⥤ U)

def inj : F.Elements ⥤ U' where
  obj | ⟨c, x⟩ => ⟨F.obj c, x⟩
  map | ⟨f, h⟩ => ⟨F.map f, h⟩

def elementsCone : Cone (@cospan Cat _ (.of C) (.of U') (.of U) F pᵤ) where
  pt := .of F.Elements
  π := {
    app := fun
    | .none => CategoryOfElements.π F ⋙ F
    | .some .left => CategoryOfElements.π F
    | .some .right => inj F
    naturality := fun _ _ => fun
    | .id _ => rfl
    | .term .left => rfl
    | .term .right => rfl }

instance : @HasPullback Cat _ (.of C) (.of U') (.of U) F pᵤ := ⟨⟨{
  cone := elementsCone F
  isLimit := {
    lift := fun ⟨pt, h⟩ => {
      obj x := ⟨(h.app .left).obj x, by
        have res := ((h.app .right).obj x).2
        have nl := h.naturality (.term .left)
        have nr := h.naturality (.term .right)
        have comm := nr.symm.trans nl
        have baz := congrArg (·.obj x) comm
        simp only [cospan_one, Cat.of_α, Functor.const_obj_obj, cospan_right,
          cospan_map_inr, Cat.comp_obj, CategoryOfElements.π_obj, Functor.id_obj,
          cospan_left, cospan_map_inl] at baz
        rw [baz] at res
        exact res⟩
      map f := ⟨(h.app (.some .left)).map f, by
        have res := ((h.app (.some .right)).map f).2
        have nl := h.naturality (.term .left)
        have nr := h.naturality (.term .right)
        have comm := nl.symm.trans nr
        simp at comm
        rw [←Functor.comp_map]
       -- rw [comm]                     ---------------- WHY wouldn't this work?

        repeat sorry
      ⟩
    }
    fac := fun ⟨pt, h⟩ => sorry
    uniq := fun ⟨pt, h⟩ => sorry }}⟩⟩
end

Any help or golfing the proofs is appreciated. I'm new to category theory in mathlib and would love to learn the proper way to do proofs such as the above.

Also, is there a way to get cospan F pᵤworking without the need for @cospan Cat ... explicitness?

[Matt Diamond]

comm is looking for h.app (some WalkingPair.left) ≫ F, while your goal contains h.app (some WalkingPair.left) ⋙ F

≫ (composition of morphisms) is not the same as ⋙ (composition of functors), so the rewrite fails

[Slavomir Kaslev]

Thank you! I'd missed the difference.
And in this particular case (category Cat), F ≫ G and F ⋙ G also happen to be equal, right?
Still wondering what a tight proof of this sorry should be like..