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))
⊢ (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)) ⋯ ⋯) ≫
        pullback.diagonal (terminal.from X) =
    ((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.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)) ⋯ ⋯

Tactic:
;

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))
⊢ (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)) ⋯ ⋯) ≫
        pullback.diagonal (terminal.from X) =
    ((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.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)) ⋯ ⋯