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.right
      ((𝟭 (Arrow C₂)).map x✝ ≫
        Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝¹).right))) ⋯)
          ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝²).right))) ⋯)
          ⋯ ≫
        (F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).map x✝)

Tactic:
apply pullback.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✝¹
⊢ Arrow.Hom.right
        ((𝟭 (Arrow C₂)).map x✝ ≫
          Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
            (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
              (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝¹).right))) ⋯)
            ⋯) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj X₁).obj x✝¹).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj X₁).obj x✝¹).right) =
    Arrow.Hom.right
        (Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
            (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
              (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝²).right))) ⋯)
            ⋯ ≫
          (F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).map x✝) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj X₁).obj x✝¹).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj X₁).obj x✝¹).right)

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.right
        ((𝟭 (Arrow C₂)).map x✝ ≫
          Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
            (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
              (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝¹).right))) ⋯)
            ⋯) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj X₁).obj x✝¹).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj X₁).obj x✝¹).right) =
    Arrow.Hom.right
        (Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
            (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
              (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝²).right))) ⋯)
            ⋯ ≫
          (F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).map x✝) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj X₁).obj x✝¹).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj X₁).obj x✝¹).right)