awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ Functor.map (Functor.obj (Functor.const WalkingCospan) t.pt) inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl

Tactic:
have w := t.π.naturality WalkingCospan.Hom.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = t.π.app WalkingCospan.left ≫ f
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Quiver.Hom (V := WalkingCospan) Option.none Option.none
none :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) Option.none ⟶ (cospan f g).obj Option.none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id Option.none) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) Option.none
        (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) Option.none
        (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id Option.none))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) Option.none ⟶ (cospan f g).obj Option.none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) Option.none
        (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) Option.none
        (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.left
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) none ⟶
      (cospan f g).obj (some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.right
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) none ⟶
      (cospan f g).obj (some WalkingPair.right))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Option.some WalkingPair.left ⟶ none
some :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.left) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map (term WalkingPair.left))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.left) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Option.some WalkingPair.left ⟶ Option.some WalkingPair.left
some :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.left) ⟶
      (cospan f g).obj (Option.some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W)
        (WidePullbackShape.Hom.id (Option.some WalkingPair.left)) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (Option.some WalkingPair.left)))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.left) ⟶
      (cospan f g).obj (Option.some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
      (cospan f g).obj (some WalkingPair.right))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Option.some WalkingPair.right ⟶ none
some :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.right) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.right) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map (term WalkingPair.right))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.right) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
      (cospan f g).obj (some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Option.some WalkingPair.right ⟶ Option.some WalkingPair.right
some :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.right) ⟶
      (cospan f g).obj (Option.some WalkingPair.right))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W)
        (WidePullbackShape.Hom.id (Option.some WalkingPair.right)) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (Option.some WalkingPair.right)))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some WalkingPair.right) ⟶
      (cospan f g).obj (Option.some WalkingPair.right))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (Option.some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (Option.some x) ⟶
            (cospan f g).obj (Option.some x))
          j' fst snd) ≫
      (cospan f g).map j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) none ⟶ (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id none) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id none))

Tactic:
simp [eq]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map (term WalkingPair.left))

Tactic:
simp [eq]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
      (cospan f g).obj (some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.left)))

Tactic:
simp [eq]