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

Goal state before:
pp: 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✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun 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))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun 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)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right)

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✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun 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))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun 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)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right)

Tactic:
<;>

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✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun 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))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun 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)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app 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✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun 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))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun 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)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right)