-- 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 f₂ ⟶ Arrow.mk sq₁₃.π
h₀ :
  sq₁₂.inl ≫
      ⋯.desc
          (((Equiv.symm adj₂.homEquiv :
                Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                  ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
              (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
            (Arrow.Hom.left β))
          (((Equiv.symm adj₂.homEquiv :
                Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                  ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
              (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
            (Arrow.Hom.right β ≫ sq₁₃.fst))
          ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
          (Arrow.Hom.right β ≫ sq₁₃.snd)
h₁ :
  sq₁₂.inr ≫
      ⋯.desc
          (((Equiv.symm adj₂.homEquiv :
                Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                  ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
              (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
            (Arrow.Hom.left β))
          (((Equiv.symm adj₂.homEquiv :
                Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                  ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
              (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
            (Arrow.Hom.right β ≫ sq₁₃.fst))
          ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inr ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
          (Arrow.Hom.right β ≫ sq₁₃.snd)
⊢ ⋯.desc
        (((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
            (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
          (Arrow.Hom.left β))
        (((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
            (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
          (Arrow.Hom.right β ≫ sq₁₃.fst))
        ⋯ ≫
      (Arrow.mk f₃).hom =
    (Arrow.mk sq₁₂.ι).hom ≫
      ((Equiv.symm adj₂.homEquiv :
            Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
              ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
          (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
        (Arrow.Hom.right β ≫ sq₁₃.snd)

Tactic:
apply sq₁₂.isPushout.hom_ext

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.IsPushout.hom_ext