-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (goal)
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₁₃.π
⊢ (fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
        (Arrow.homMk
            (((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 α))
            (⋯.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 α))
              ⋯)
            ⋯ :
          Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
      ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
          (Arrow.homMk
              (⋯.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))
                ⋯)
              (((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))
              ⋯ :
            Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
        β) =
    β
have h₁ : Arrow.Hom.left
    ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
        (Arrow.homMk
            (((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 α))
            (sorry.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 α))
              sorry)
            sorry :
          Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
      ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
          (Arrow.homMk
              (sorry.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))
                sorry)
              (((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))
              sorry :
            Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
        β)) =
  Arrow.Hom.left β
Tactic: ext