Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
w✝⁴ : C
w✝³ : w✝⁴ ⟶ a
w✝² : F.obj w✝⁴ ⟶ F.obj a
pbRepr :
  IsPullback w✝² (F.map w✝³) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
toCommSq✝ :
  CommSq
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ D)) ⋯ ⋯))
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ 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))
      (𝟙 (⊤_ D)) ⋯ ⋯)
bot :
  IsLimit
    (PullbackCone.mk
      ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        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)) (𝟙 (⊤_ D)) ⋯ ⋯))
      ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        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)) (𝟙 (⊤_ D)) ⋯ ⋯))
      ⋯)
w✝¹ : C
w✝ : w✝¹ ⟶ w✝⁴
topMap : F.obj w✝¹ ⟶ F.obj a
top :
  IsPullback topMap (F.map w✝) (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯)
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ D)) ⋯ ⋯))
⊢ ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g

Tactic:
have hg : g = pullback.lift (𝟙 _) (𝟙 _) (by cat_disch) ≫ pullback.map
    ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X) _ _
      (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _) (𝟙 _) (by cat_disch) (by cat_disch) := by
    apply Limits.pullback.hom_ext <;> simp

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
w✝⁴ : C
w✝³ : w✝⁴ ⟶ a
w✝² : F.obj w✝⁴ ⟶ F.obj a
pbRepr :
  IsPullback w✝² (F.map w✝³) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
toCommSq✝ :
  CommSq
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ D)) ⋯ ⋯))
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ 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))
      (𝟙 (⊤_ D)) ⋯ ⋯)
bot :
  IsLimit
    (PullbackCone.mk
      ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        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)) (𝟙 (⊤_ D)) ⋯ ⋯))
      ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        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)) (𝟙 (⊤_ D)) ⋯ ⋯))
      ⋯)
w✝¹ : C
w✝ : w✝¹ ⟶ w✝⁴
topMap : F.obj w✝¹ ⟶ F.obj a
top :
  IsPullback topMap (F.map w✝) (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯)
    ((pbRepr.isoPullback ≪≫
          (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
              (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
      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))
          (𝟙 (⊤_ D)) ⋯ ⋯))
hg :
  g =
    pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫
      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))
        (𝟙 (⊤_ D)) ⋯ ⋯
⊢ ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g