awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f_1 ≫ inl = g ≫ inr
f : some WalkingPair.left ⟶ none
⊢ Eq (α :=
    (span f_1 g).obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) none)
    ((span f_1 g).map f ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f_1 ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.left) (f_1 ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) f)

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

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

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

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

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

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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
none : f ≫ inl = (f ≫ inl) ≫ 𝟙 W
⊢ Eq (α :=
    (span f g).obj Option.none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((span f g).map (init WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) Option.none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (init WalkingPair.left))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
none : g ≫ inr = (f ≫ inl) ≫ 𝟙 W
⊢ Eq (α :=
    (span f g).obj Option.none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((span f g).map (init WalkingPair.right) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) Option.none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (init WalkingPair.right))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
some : (span f g).map (𝟙 (Option.some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W
⊢ Eq (α :=
    (span f g).obj (Option.some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (Option.some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (Option.some x) ⟶
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some x))
          j' inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (Option.some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (Option.some x) ⟶
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some x))
          j' inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (WidePushoutShape.Hom.id (Option.some WalkingPair.left)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
some : (span f g).map (𝟙 (Option.some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W
⊢ Eq (α :=
    (span f g).obj (Option.some WalkingPair.right) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.id (Option.some WalkingPair.right)) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (Option.some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (Option.some x) ⟶
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some x))
          j' inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (Option.some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f g).obj (Option.some x) ⟶
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (Option.some x))
          j' inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (WidePushoutShape.Hom.id (Option.some WalkingPair.right)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 none) ≫ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ g ≫ inr = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (mk inl inr eq).ι.app WalkingSpan.left = inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (mk inl inr eq).ι.app WalkingSpan.right = inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (mk inl inr eq).ι.app WalkingSpan.zero = f ≫ inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (mk inl inr eq).inl = inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (mk inl inr eq).inr = inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ f ≫ t.inl = g ≫ t.inr

Tactic:
(t.w fst).trans (t.w snd).symm

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingSpan.Hom.fst, CategoryTheory.Limits.WalkingSpan.Hom.snd, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
rw : ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
rw₁ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
rw₂ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
rw₃ rw₄ : (span f g).map fst ≫ t.inl ≫ l = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
⊢ Eq (α := (span f g).obj none ⟶ W) (t.ι.app none ≫ k) (t.ι.app none ≫ l)

Tactic:
rw [← t.w fst, Category.assoc, Category.assoc, h₀]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
desc : (s : PushoutCocone f g) → t.pt ⟶ s.pt
fac_left : ∀ (s : PushoutCocone f g), t.inl ≫ desc s = s.inl
fac_right : ∀ (s : PushoutCocone f g), t.inr ≫ desc s = s.inr
uniq : ∀ (s : PushoutCocone f g) (m : t.pt ⟶ s.pt), (∀ (j : WalkingSpan), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (span f g)
j : WalkingSpan
⊢ Eq (α := (span f g).obj none ⟶ s.pt) (t.ι.app none ≫ desc s) (s.ι.app none)

Tactic:
simp [← s.w fst, ← t.w fst, fac_left s]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ k = l

Tactic:
ht.hom_ext <| coequalizer_ext _ h₀ h₁

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.PushoutCocone.coequalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ t.inl ≫ desc ht h k w = h

Tactic:
ht.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ t.inr ≫ desc ht h k w = k

Tactic:
ht.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ t.inl ≫ desc ht h k w = h ∧ t.inr ≫ desc ht h k w = k

Tactic:
simp