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 : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.right) ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map (term WalkingPair.right))

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

Tactic:
simp [eq]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (mk fst snd eq).π.app WalkingCospan.left = fst

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 ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (mk fst snd eq).π.app WalkingCospan.right = snd

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 ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (mk fst snd eq).π.app WalkingCospan.one = fst ≫ f

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 ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (mk fst snd eq).fst = fst

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 ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (mk fst snd eq).snd = snd

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.fst ≫ f = t.snd ≫ g

Tactic:
(t.w inl).trans (t.w inr).symm

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingCospan.Hom.inr, 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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
rw : k ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl = l ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl
rw₁ rw₂ : l ≫ t.fst ≫ (cospan f g).map inl = l ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ Eq (α := W ⟶ (cospan f g).obj none) (k ≫ t.π.app none) (l ≫ t.π.app none)

Tactic:
rw [← t.w inl, reassoc_of% h₀]

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
rw : (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ Eq (α := s.pt ⟶ (cospan f g).obj none) (lift s ≫ t.π.app none) (s.π.app none)

Tactic:
rw [← s.w inl, ← t.w inl, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
e_a : lift s ≫ t.π.app WalkingCospan.left = s.π.app WalkingCospan.left
⊢ (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app WalkingCospan.left = s.π.app WalkingCospan.left

Tactic:
fac_left s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app WalkingCospan.left = s.π.app WalkingCospan.left

Tactic:
exact fac_left s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
⊢ k = l

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

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

Tactic:
ht.fac _ _

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

Tactic:
ht.fac _ _

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.pt = t.pt

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.cospan, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.fst = t.snd

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.snd = t.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.fst = Iso.hom (Iso.refl t.flip.flip.pt) ≫ t.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.snd = Iso.hom (Iso.refl t.flip.flip.pt) ≫ t.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.snd = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.fst = s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
h₀ : m ≫ t.fst = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.fst
h₃ : m ≫ t.snd = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.snd
⊢ m = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s

Tactic:
apply IsLimit.hom_ext ht

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.fst = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.fst

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.snd = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.snd

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingCospan C
t : Cone F
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingCospan) ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt) none ⟶
      (cospan (F.map inl) (F.map inr)).obj none)
    (((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app none)
    (Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt) ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingCospan C
t : Cone F
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingCospan) ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt)
        (some WalkingPair.left) ⟶
      (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left))
    (((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.left))
    (Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt) ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingCospan C
t : Cone F
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingCospan) ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt)
        (some WalkingPair.right) ⟶
      (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right))
    (((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.right))
    (Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt) ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.right))

Tactic:
simp
-- 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
c : PushoutCocone f g
⊢ c.ι.app WalkingSpan.left = c.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
c : PushoutCocone f g
⊢ c.ι.app WalkingSpan.right = c.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
⊢ (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ Functor.map (Functor.obj (Functor.const WalkingSpan) t.pt) fst

Tactic:
have w := t.ι.naturality 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
w : f ≫ t.ι.app WalkingSpan.left = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
simpa using w.symm

Premises used: Eq.symm
-- 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 : Quiver.Hom (V := WalkingSpan) Option.none Option.none
none :
  Eq (α :=
    (span f_1 g).obj Option.none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) Option.none)
    ((span f_1 g).map (WidePushoutShape.Hom.id Option.none) ≫
      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.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) Option.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) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (WidePushoutShape.Hom.id Option.none))
⊢ Eq (α :=
    (span f_1 g).obj Option.none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) Option.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) Option.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) Option.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) ≫
      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.none ⟶ some WalkingPair.left
none :
  Eq (α :=
    (span f_1 g).obj Option.none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((span f_1 g).map (init 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)
        (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) Option.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) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (init WalkingPair.left))
⊢ Eq (α :=
    (span f_1 g).obj Option.none ⟶
      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) Option.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) ≫
      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.none ⟶ some WalkingPair.right
none :
  Eq (α :=
    (span f_1 g).obj Option.none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((span f_1 g).map (init 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)
        (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) Option.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) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) (init WalkingPair.right))
⊢ Eq (α :=
    (span f_1 g).obj Option.none ⟶
      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) Option.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) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) f)

Tactic:
cases f