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

Goal state before:
pp: case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
f : none ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases f

Goal state after:
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ (F.map (Hom.id none) ≫
      match none with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : none ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases f

Goal state after:
case none.some.init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ (F.map (Hom.init val✝) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match some val✝ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match some val✝¹ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases f

Goal state after:
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ (F.map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match some val✝ with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id (some val✝))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f

Goal state after:
case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
cases f

Goal state after:
case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ none
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case none.none.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case some.left.none.term
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.left) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case some.right.none.term
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.right) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (cospan f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case some.right.some.right.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.right))