Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.left
      ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
        Arrow.homMk
          (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
            (adj₂.homEquiv.symm
              (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
            ⋯)
          (adj₂.homEquiv.symm
            (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom) ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
          ⋯) =
    Arrow.Hom.left
      (Arrow.homMk
          (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
            (adj₂.homEquiv.symm
              (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                ((G.map (unop (op X₁)).hom.op).app x✝².right)))
            ⋯)
          (adj₂.homEquiv.symm
            (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom) ((G.map (unop (op X₁)).hom.op).app x✝².right)))
          ⋯ ≫
        (𝟭 (Arrow C₃)).map x✝)

Tactic:
apply pushout.hom_ext

Goal state after:
case h₁.h₀
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ pushout.inl ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
          Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
            ⋯) =
    pushout.inl ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        (Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝².right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                ((G.map (unop (op X₁)).hom.op).app x✝².right)))
            ⋯ ≫
          (𝟭 (Arrow C₃)).map x✝)

case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
          Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
            ⋯) =
    pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        (Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝².right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                ((G.map (unop (op X₁)).hom.op).app x✝².right)))
            ⋯ ≫
          (𝟭 (Arrow C₃)).map x✝)