mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map (pushout.inl f g) ≫ (iso G f g).inv = pushout.inl (G.map f) (G.map g)

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map (pushout.inr f g) ≫ (iso G f g).inv = pushout.inr (G.map f) (G.map g)

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Goal state after:
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

Tactic:
cases f

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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id none) ≫
      (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 (WidePushoutShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
case none.some.left.init
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
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      (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 (WidePushoutShape.Hom.init WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
case none.some.right.init
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
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      (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 (WidePushoutShape.Hom.init WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (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 (WidePushoutShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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:
cases f

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (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 (WidePushoutShape.Hom.id (some WalkingPair.right))
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 ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

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.op g.op).map (WidePullbackShape.Hom.id none) ≫
      (match none with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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 ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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 ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
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.op g.op).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (match none with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.term WalkingPair.left)