-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X)
w : C
w_1 : w ⟶ a
w_2 : F.obj w ⟶ F.obj a
pbRepr :
  IsPullback w_2 (F.map w_1) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
toCommSq :
  CommSq (Y :=
    Limits.pullback (Z := terminal.{v₂, u₂} D)
      ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
      ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
    (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
    (CategoryStruct.comp (Y :=
      Limits.pullback (Y :=
        Limits.pullback (Z := terminal.{v₂, u₂} D)
          ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
        (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
        (pullback.diagonal (terminal.from X))
        (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
          (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
          (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯))
      (Iso.hom
        (Iso.trans (Y :=
          Limits.pullback (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)))
          pbRepr.isoPullback
          (Iso.symm
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)))))
      (pullback.fst (pullback.diagonal (terminal.from X))
        (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
          (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
          (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)))
    (CategoryStruct.comp (Y :=
      Limits.pullback (Y :=
        Limits.pullback (Z := terminal.{v₂, u₂} D)
          ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
        (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
        (pullback.diagonal (terminal.from X))
        (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
          (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
          (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯))
      (Iso.hom
        (Iso.trans (Y :=
          Limits.pullback (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)))
          pbRepr.isoPullback
          (Iso.symm
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)))))
      (pullback.snd (pullback.diagonal (terminal.from X))
        (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
          (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
          (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)))
    (pullback.diagonal (terminal.from X))
    (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
      ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
      (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
      (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)
bot :
  IsLimit
    (PullbackCone.mk
      (CategoryStruct.comp (Y :=
        Limits.pullback (Y :=
          Limits.pullback (Z := terminal.{v₂, u₂} D)
            ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
          (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
          (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯))
        (Iso.hom
          (Iso.trans (Y :=
            Limits.pullback (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)))
            pbRepr.isoPullback
            (Iso.symm
              (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)))))
        (pullback.fst (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)))
      (CategoryStruct.comp (Y :=
        Limits.pullback (Y :=
          Limits.pullback (Z := terminal.{v₂, u₂} D)
            ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
          (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
          (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯))
        (Iso.hom
          (Iso.trans (Y :=
            Limits.pullback (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)))
            pbRepr.isoPullback
            (Iso.symm
              (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)))))
        (pullback.snd (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)))
      ⋯)
obtain :
  ∀ (w_3 : C) (w_4 : w_3 ⟶ w) (topMap : F.obj w_3 ⟶ F.obj a)
    (top :
      IsPullback (Z :=
        Limits.pullback (Z := terminal.{v₂, u₂} D)
          ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
        topMap (F.map w_4)
        (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ :
          F.obj a ⟶
            Limits.pullback (Z := terminal.{v₂, u₂} D)
              ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
              ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
        (CategoryStruct.comp (Y :=
            Limits.pullback (Y :=
              Limits.pullback (Z := terminal.{v₂, u₂} D)
                ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
                ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
              (Z := pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X))
              (pullback.diagonal (terminal.from X))
              (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
                ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
                (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯))
            (Iso.hom
              (Iso.trans (Y :=
                Limits.pullback (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                  (g ≫ pullback.snd (terminal.from X) (terminal.from X)))
                pbRepr.isoPullback
                (Iso.symm
                  (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                    (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)))))
            (pullback.snd (pullback.diagonal (terminal.from X))
              (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
                ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
                (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)) :
          F.obj w ⟶
            Limits.pullback (Z := terminal.{v₂, u₂} D)
              ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
              ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))),
    ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g

Tactic:
obtain ⟨_, ⟨_, ⟨topMap, top⟩⟩⟩ := (toPullbackTerminal g) <|
    (pbRepr.isoPullback ≪≫ (pullbackDiagonalMapIdIso (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
      (terminal.from X)).symm).hom ≫ pullback.snd
        (pullback.diagonal (terminal.from X))
        (pullback.map _ _ _ _ _ _ (𝟙 _) (by cat_disch) (by cat_disch))

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.terminal.from, CategoryTheory.IsPullback.isoPullback, CategoryTheory.Limits.pullback.map, CategoryTheory.Iso.trans, CategoryTheory.Limits.pullback.fst, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pullback.diagonal, CategoryTheory.Iso.hom, CategoryTheory.Limits.pullbackDiagonalMapIdIso, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal