awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : Quiver.Hom (V := WalkingCospan) Option.none Option.none
none :
  Eq (α := (cospan f_1 g ⋙ F).obj Option.none ⟶ (cospan (F.map f_1) (F.map g)).obj Option.none)
    ((cospan f_1 g ⋙ F).map (WidePullbackShape.Hom.id Option.none) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) Option.none
          (Iso.refl ((cospan f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) Option.none
          (Iso.refl ((cospan f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map (WidePullbackShape.Hom.id Option.none))
⊢ Eq (α := (cospan f_1 g ⋙ F).obj Option.none ⟶ (cospan (F.map f_1) (F.map g)).obj Option.none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) Option.none
          (Iso.refl ((cospan f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) Option.none
          (Iso.refl ((cospan f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ Eq (α := (cospan f_1 g ⋙ F).obj none ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ Eq (α := (cospan f_1 g ⋙ F).obj none ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : Option.some WalkingPair.left ⟶ none
some :
  Eq (α := (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map (term WalkingPair.left) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map (term WalkingPair.left))
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : Option.some WalkingPair.right ⟶ none
some :
  Eq (α := (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map (term WalkingPair.right) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map (term WalkingPair.right))
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := (cospan f g ⋙ F).obj none ⟶ (cospan (F.map f) (F.map g)).obj none)
    ((cospan f g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) none (Iso.refl ((cospan f g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) none (Iso.refl ((cospan f g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id none))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := (cospan f g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f) (F.map g)).obj none)
    ((cospan f g ⋙ F).map (term WalkingPair.left) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) none (Iso.refl ((cospan f g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := (cospan f g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f) (F.map g)).obj (some WalkingPair.left))
    ((cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := (cospan f g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f) (F.map g)).obj none)
    ((cospan f g ⋙ F).map (term WalkingPair.right) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) none (Iso.refl ((cospan f g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := (cospan f g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f) (F.map g)).obj (some WalkingPair.right))
    ((cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f g ⋙ F).obj x ≅ (cospan (F.map f) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f g ⋙ F).obj (some x) ≅ (cospan (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.right)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospanCompIso F f g).app WalkingCospan.left = Iso.refl ((cospan f g ⋙ F).obj WalkingCospan.left)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospanCompIso F f g).app WalkingCospan.right = Iso.refl ((cospan f g ⋙ F).obj WalkingCospan.right)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospanCompIso F f g).app WalkingCospan.one = Iso.refl ((cospan f g ⋙ F).obj WalkingCospan.one)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospanCompIso F f g).hom.app WalkingCospan.left = 𝟙 ((cospan f g ⋙ F).obj WalkingCospan.left)

Tactic:
rfl

Premises used: rfl