awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (span f_1.op g.op) (some WalkingPair.left) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj none)
    (map (span f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          none))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.left)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (span f_1.op g.op) (some WalkingPair.left) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj (some WalkingPair.right))
    (map (span f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.left)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (span f_1.op g.op) (some WalkingPair.right) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj none)
    (map (span f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          none))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.right)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (span f_1.op g.op) (some WalkingPair.right) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj (some WalkingPair.left))
    (map (span f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f_1.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f_1.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).obj x))
          (some WalkingPair.right)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ Eq (α :=
    (span f_1.unop g.unop).obj (some WalkingPair.left) ⟶
      obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) none)
    ((span f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          none))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.left)) ≫
      map (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α :=
    (span f_1.unop g.unop).obj (some WalkingPair.left) ⟶
      obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) (some WalkingPair.right))
    ((span f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.left)) ≫
      map (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ Eq (α :=
    (span f_1.unop g.unop).obj (some WalkingPair.right) ⟶
      obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) none)
    ((span f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          none))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.right)) ≫
      map (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α :=
    (span f_1.unop g.unop).obj (some WalkingPair.right) ⟶
      obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) (some WalkingPair.left))
    ((span f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  (span f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x)
                x with
              | none => Iso.refl ((span f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.left)
              | some WalkingPair.right => Iso.refl ((span f_1.unop g.unop).obj WalkingSpan.right) :
              (span f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) x))
          (some WalkingPair.right)) ≫
      map (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none ⟶
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj (some WalkingPair.left))
    (map (cospan f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          none) ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none ⟶
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj (some WalkingPair.right))
    (map (cospan f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          none) ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) (some WalkingPair.left) ⟶
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj (some WalkingPair.right))
    (map (cospan f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.left)) ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) (some WalkingPair.right) ⟶
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj (some WalkingPair.left))
    (map (cospan f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          (some WalkingPair.right)) ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map f)

Tactic:
cases f