mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case none.some.left.init
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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (init WalkingPair.left) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

Tactic:
cases f

Goal state after:
case none.some.right.init
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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (init WalkingPair.right) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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.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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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.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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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 ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (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 ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.right))
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 : none ⟶ none
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

Goal state after:
case none.none.id
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
⊢ ((span f g).map (WidePushoutShape.Hom.id none) ≫
      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 (WidePushoutShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
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 : none ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : none ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.left ⟶ none
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.left ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.left ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.right ⟶ none
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.right ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
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 : some WalkingPair.right ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ 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

Tactic:
cases f

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

Goal state before:
pp: X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
⊢ f.comp (id Y) = f

Tactic:
cases f

Goal state after:
case left
⊢ left.comp (id one) = left

case right
⊢ right.comp (id one) = right

case id
X : WalkingParallelPair
⊢ (id X).comp (id X) = id X
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
cases f

Goal state after:
case left
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (left.comp g).comp h = left.comp (g.comp h)

case right
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (right.comp g).comp h = right.comp (g.comp h)

case id
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
⊢ ((id X).comp g).comp h = (id X).comp (g.comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: X✝ Y✝ : WalkingParallelPair
f : X✝ ⟶ Y✝
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match Y✝ with
      | zero => one
      | one => zero)

Tactic:
cases f

Goal state after:
case left
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

case right
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

case id
X✝ : WalkingParallelPair
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match X✝ with
      | zero => one
      | one => zero)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Under X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Under (F.obj X)
B' : T
e : F.obj B' ≅ B.right
⊢ (post F).essImage B

Tactic:
obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Under (F.obj X)
B' : T
e : F.obj B' ≅ B.right
f : X ⟶ B'
hf : F.map f = B.hom ≫ e.inv
⊢ (post F).essImage B
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Under X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (mk (unop Y).hom.op).hom = (mk (unop Z).hom.op).hom

Tactic:
by dsimp; rw [← Under.w f.unop, op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤

Tactic:
· intro
    ext X Y f
    simp only [top_apply, iff_true]
    exact ⟨factorizationData W₁ W₂ f⟩

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ ∀ {X_1 Y_1 Z : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1) (g_1 : Y_1 ⟶ Z),
    parallelPairHom f g (f_1 ≫ g_1) = parallelPairHom f g f_1 ≫ parallelPairHom f g g_1

Tactic:
by rintro _ _ _ ⟨⟩ ⟨⟩ <;> simp

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

Goal state before:
pp: case zero.zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : zero ⟶ zero
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases f

Goal state after:
case zero.zero.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id zero) ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id zero)