-- 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
X : D
h :
  F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X)
    (CategoryStruct.comp (Y := Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
        X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (Iso.inv (prodIsoPullback X X) :
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
          Limits.prod.{v₂, u₂} X X))
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq :
  CommSq (W := Limits.pullback g g') (Y :=
    Limits.pullback (Z := terminal.{v₂, u₂} D) (g ≫ terminal.from X) (g' ≫ terminal.from X)) (Z :=
    pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X)) (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g'
      (𝟙 (terminal.{v₂, u₂} D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (Limits.prod.{v₁, u₁} a a') ⟶ Limits.prod.{v₂, u₂} X X :=
  CategoryStruct.comp (Y := limit.{0, 0, v₂, u₂} (pair (F.obj a) (F.obj a')))
    (Iso.hom
      (Iso.trans (Y := limit (pair a a' ⋙ F))
        (preservesLimitIso F (pair a a') : F.obj (limit.{0, 0, v₁, u₁} (pair a a')) ≅ limit (pair a a' ⋙ F))
        (HasLimit.isoOfNatIso (pairComp a a' F) :
          limit (pair a a' ⋙ F) ≅ limit.{0, 0, v₂, u₂} (pair (F.obj a) (F.obj a')))))
    (prod.map g g')
pbRepr : (PullbackCone.mk
      (⋯.choose (p :=
        fun
          (fst :
            F.obj
                (⋯.choose (p := fun (b : C) ↦
                  ∃ (snd : b ⟶ Limits.prod.{v₁, u₁} a a') (fst : F.obj b ⟶ X),
                    IsPullback fst (F.map snd)
                      (CategoryStruct.comp (Y :=
                        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                          X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (Iso.inv (prodIsoPullback X X) :
                          Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                            Limits.prod.{v₂, u₂} X X))
                      prodMap)) ⟶
              X) ↦
        IsPullback fst
          (F.map
            (⋯.choose (p :=
              fun
                (snd :
                  ⋯.choose (p := fun (b : C) ↦
                      ∃ (snd : b ⟶ Limits.prod.{v₁, u₁} a a') (fst : F.obj b ⟶ X),
                        IsPullback fst (F.map snd)
                          (CategoryStruct.comp (Y :=
                            Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                            (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                              X ⟶
                                Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                            (Iso.inv (prodIsoPullback X X) :
                              Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                                Limits.prod.{v₂, u₂} X X))
                          prodMap) ⟶
                    Limits.prod.{v₁, u₁} a a') ↦
              ∃ (fst :
                F.obj
                    (⋯.choose (p := fun (b : C) ↦
                      ∃ (snd : b ⟶ Limits.prod.{v₁, u₁} a a') (fst : F.obj b ⟶ X),
                        IsPullback fst (F.map snd)
                          (CategoryStruct.comp (Y :=
                            Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                            (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                              X ⟶
                                Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                            (Iso.inv (prodIsoPullback X X) :
                              Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                                Limits.prod.{v₂, u₂} X X))
                          prodMap)) ⟶
                  X),
                IsPullback fst (F.map snd)
                  (CategoryStruct.comp (Y :=
                    Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                    (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                      X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                    (Iso.inv (prodIsoPullback X X) :
                      Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                        Limits.prod.{v₂, u₂} X X))
                  prodMap)))
          (CategoryStruct.comp (Y :=
            Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
            (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
              X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
            (Iso.inv (prodIsoPullback X X) :
              Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                Limits.prod.{v₂, u₂} X X))
          prodMap))
      (F.map
        (⋯.choose (p :=
          fun
            (snd :
              ⋯.choose (p := fun (b : C) ↦
                  ∃ (snd : b ⟶ Limits.prod.{v₁, u₁} a a') (fst : F.obj b ⟶ X),
                    IsPullback fst (F.map snd)
                      (CategoryStruct.comp (Y :=
                        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                          X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (Iso.inv (prodIsoPullback X X) :
                          Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                            Limits.prod.{v₂, u₂} X X))
                      prodMap) ⟶
                Limits.prod.{v₁, u₁} a a') ↦
          ∃ (fst :
            F.obj
                (⋯.choose (p := fun (b : C) ↦
                  ∃ (snd : b ⟶ Limits.prod.{v₁, u₁} a a') (fst : F.obj b ⟶ X),
                    IsPullback fst (F.map snd)
                      (CategoryStruct.comp (Y :=
                        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                          X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                        (Iso.inv (prodIsoPullback X X) :
                          Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                            Limits.prod.{v₂, u₂} X X))
                      prodMap)) ⟶
              X),
            IsPullback fst (F.map snd)
              (CategoryStruct.comp (Y :=
                Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
                  X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                (Iso.inv (prodIsoPullback X X) :
                  Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
                    Limits.prod.{v₂, u₂} X X))
              prodMap)))
      ⋯).pt ≅
  Cone.pt (F :=
    cospan
      (CategoryStruct.comp (Y :=
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
        (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
          X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
        (Iso.inv (prodIsoPullback X X) :
          Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
            Limits.prod.{v₂, u₂} X X))
      prodMap)
    (PullbackCone.pasteHoriz
      (PullbackCone.mk (W := Limits.pullback (Z := terminal.{v₂, u₂} D) (g ≫ terminal.from X) (g' ≫ terminal.from X))
        ((limit.isLimit (cospan (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X)) :
              IsLimit.{0, v₂, 0, u₂} (F := cospan (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
                (limit.cone (cospan (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X)))).1
          (PullbackCone.mk (W :=
            Limits.pullback (Z := terminal.{v₂, u₂} D) (g ≫ terminal.from X) (g' ≫ terminal.from X))
            (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
            (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
        (Iso.hom
          (Iso.trans (Y :=
            Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a)) (terminal.from (F.obj a')))
            (pullback.congrHom ⋯ ⋯ :
              Limits.pullback (Z := terminal.{v₂, u₂} D) (g ≫ terminal.from X) (g' ≫ terminal.from X) ≅
                Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a))
                  (terminal.from (F.obj a')))
            (Iso.trans (Y := Limits.prod.{v₂, u₂} (F.obj a) (F.obj a'))
                (Iso.symm (prodIsoPullback (F.obj a) (F.obj a')))
                (Iso.trans (Y := limit (pair a a' ⋙ F))
                  (Iso.symm (HasLimit.isoOfNatIso (pairComp a a' F)) :
                    limit.{0, 0, v₂, u₂} (pair (F.obj a) (F.obj a')) ≅ limit (pair a a' ⋙ F))
                  (Iso.symm (preservesLimitIso F (pair a a')) :
                    limit (pair a a' ⋙ F) ≅ F.obj (limit.{0, 0, v₁, u₁} (pair a a')))) :
              Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a)) (terminal.from (F.obj a')) ≅
                F.obj (limit.{0, 0, v₁, u₁} (pair a a')))))
        ⋯)
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯) :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ (Nonempty.some ⋯) left)
⊢ (pbRepr.hom ≫ pullback.fst g g') ≫ g = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g')) ≫ g'

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition