Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
<;>

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case none.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case none.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.left.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.right.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j