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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : none ⟶ none),
    ((span f g).map f_1 ≫ Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

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

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

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.left ⟶ some WalkingPair.left),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

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

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

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

case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.right ⟶ some WalkingPair.right),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1