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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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