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

Goal state before:
pp: case refine_2
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)
k : D
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (c k)).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
                (c k)).pt).hom ≫
        (((evaluation D C).obj k).mapCone (combine f g c hc)).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case refine_2.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)
k : D
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (c k)).π.app
      none =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (c k)).pt).hom ≫
      (((evaluation D C).obj k).mapCone (combine f g c hc)).π.app none

case refine_2.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)
k : D
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (c k)).π.app
      (some WalkingPair.left) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (c k)).pt).hom ≫
      (((evaluation D C).obj k).mapCone (combine f g c hc)).π.app (some WalkingPair.left)

case refine_2.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)
k : D
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (c k)).π.app
      (some WalkingPair.right) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (c k)).pt).hom ≫
      (((evaluation D C).obj k).mapCone (combine f g c hc)).π.app (some WalkingPair.right)