-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
h₀ :
  (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
          (sq₁₂.inl ≫ Arrow.Hom.left α) ≫
        (Arrow.mk sq₁₃.π).hom) ≫
      sq₁₃.fst =
    ((Arrow.mk f₂).hom ≫
        ⋯.lift
          (((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
              (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
            (sq₁₂.inr ≫ Arrow.Hom.left α))
          (((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
            (Arrow.Hom.right α))
          ⋯) ≫
      sq₁₃.fst
h₁ :
  (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
          (sq₁₂.inl ≫ Arrow.Hom.left α) ≫
        (Arrow.mk sq₁₃.π).hom) ≫
      sq₁₃.snd =
    ((Arrow.mk f₂).hom ≫
        ⋯.lift
          (((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
              (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
            (sq₁₂.inr ≫ Arrow.Hom.left α))
          (((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
            (Arrow.Hom.right α))
          ⋯) ≫
      sq₁₃.snd
⊢ ((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
              ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
          (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
        (sq₁₂.inl ≫ Arrow.Hom.left α) ≫
      (Arrow.mk sq₁₃.π).hom =
    (Arrow.mk f₂).hom ≫
      ⋯.lift
        (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
            (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
          (sq₁₂.inr ≫ Arrow.Hom.left α))
        (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
            (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
          (Arrow.Hom.right α))
        ⋯

Tactic:
apply sq₁₃.isPullback.hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.Functor.PullbackObjObj.isPullback