Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app none =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app none

pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.left) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.left)

pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.right) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.right)

Tactic:
;

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app none =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app none

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.left) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.right) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.right)