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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
              whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
          x✝) ≫
      pullback.fst ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj x✝).right) =
    Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
              (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
          x✝) ≫
      pullback.fst ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj 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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
              whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
          x✝) ≫
      pullback.snd ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj x✝).right) =
    Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
              (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
          x✝) ≫
      pullback.snd ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj 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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
              whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
          x✝) ≫
      pullback.fst ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj x✝).right) =
    Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
              (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
          x✝) ≫
      pullback.fst ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
              whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
          x✝) ≫
      pullback.snd ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj x✝).right) =
    Arrow.Hom.right
        (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
              (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
          x✝) ≫
      pullback.snd ((G.obj (op (unop (op X₁✝)).left)).map ((F.leibnizPushout.obj Y₁✝).obj x✝).hom)
        ((G.map (unop (op X₁✝)).hom.op).app ((F.leibnizPushout.obj Y₁✝).obj x✝).right)