Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

pp: case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

Tactic:
<;>

Goal state after:
case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f

case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).leftOp).map f