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 : X ⟶ Z
g : Y ⟶ Z
⊢ (cospanCompIso F f g).hom.app WalkingCospan.right = 𝟙 ((cospan f g ⋙ F).obj WalkingCospan.right)

Tactic:
rfl

Premises used: 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.one = 𝟙 ((cospan f g ⋙ F).obj WalkingCospan.one)

Tactic:
rfl

Premises used: 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).inv.app WalkingCospan.left = 𝟙 ((cospan (F.map f) (F.map g)).obj WalkingCospan.left)

Tactic:
rfl

Premises used: 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).inv.app WalkingCospan.right = 𝟙 ((cospan (F.map f) (F.map g)).obj WalkingCospan.right)

Tactic:
rfl

Premises used: 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).inv.app WalkingCospan.one = 𝟙 ((cospan (F.map f) (F.map g)).obj WalkingCospan.one)

Tactic:
rfl

Premises used: 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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).obj none ≅ (span (F.map f) (F.map g)).obj none

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).obj (some WalkingPair.left) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.left)

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).obj (some WalkingPair.right) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.right)

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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 ⟶ Y
g : X ⟶ Z
f : Quiver.Hom (V := WalkingSpan) Option.none Option.none
none :
  Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj Option.none)
    ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id Option.none) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id Option.none))
⊢ Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj Option.none)
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : Option.none ⟶ some WalkingPair.left
none :
  Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((span f_1 g ⋙ F).map (init WalkingPair.left) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map (init WalkingPair.left))
⊢ Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : Option.none ⟶ some WalkingPair.right
none :
  Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((span f_1 g ⋙ F).map (init WalkingPair.right) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map (init WalkingPair.right))
⊢ Eq (α := (span f_1 g ⋙ F).obj Option.none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          Option.none (Iso.refl ((span f_1 g ⋙ F).obj Option.none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (span (F.map f_1) (F.map g)).obj none)
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : Option.some WalkingPair.left ⟶ Option.some WalkingPair.left
some :
  Eq (α :=
    (span f_1 g ⋙ F).obj (Option.some WalkingPair.left) ⟶
      (span (F.map f_1) (F.map g)).obj (Option.some WalkingPair.left))
    ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)))
⊢ Eq (α :=
    (span f_1 g ⋙ F).obj (Option.some WalkingPair.left) ⟶
      (span (F.map f_1) (F.map g)).obj (Option.some WalkingPair.left))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (span (F.map f_1) (F.map g)).obj none)
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : Option.some WalkingPair.right ⟶ Option.some WalkingPair.right
some :
  Eq (α :=
    (span f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶
      (span (F.map f_1) (F.map g)).obj (Option.some WalkingPair.right))
    ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id (Option.some WalkingPair.right)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id (Option.some WalkingPair.right)))
⊢ Eq (α :=
    (span f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶
      (span (F.map f_1) (F.map g)).obj (Option.some WalkingPair.right))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (Option.some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (Option.some x) ≅ (span (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)

Tactic:
cases f