mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.left
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

pp: case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.right
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.left
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.right
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
⊢ (𝟭 WalkingParallelPair).obj zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero

pp: case one
⊢ (𝟭 WalkingParallelPair).obj one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one

Tactic:
<;>

Goal state after:
case zero
⊢ (𝟭 WalkingParallelPair).obj zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero

case one
⊢ (𝟭 WalkingParallelPair).obj one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
⊢ (𝟭 WalkingParallelPair).map left ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map left

pp: case right
⊢ (𝟭 WalkingParallelPair).map right ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map right

pp: case id
X✝ : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
⊢ (𝟭 WalkingParallelPair).map left ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map left

case right
⊢ (𝟭 WalkingParallelPair).map right ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map right

case id
X✝ : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.zero
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = (𝟭 WalkingParallelPairᵒᵖ).obj (op zero)

pp: case op.one
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) = (𝟭 WalkingParallelPairᵒᵖ).obj (op one)

Tactic:
<;>

Goal state after:
case op.zero
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = (𝟭 WalkingParallelPairᵒᵖ).obj (op zero)

case op.one
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) = (𝟭 WalkingParallelPairᵒᵖ).obj (op one)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
have : f = g.op := rfl

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op.zero
j : WalkingParallelPair
f : op zero ⟶ op j
g : unop (op j) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

pp: case op.op.one
j : WalkingParallelPair
f : op one ⟶ op j
g : unop (op j) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
<;>

Goal state after:
case op.op.zero
j : WalkingParallelPair
f : op zero ⟶ op j
g : unop (op j) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.one
j : WalkingParallelPair
f : op one ⟶ op j
g : unop (op j) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op.zero.zero
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

pp: case op.op.zero.one
f : op zero ⟶ op one
g : unop (op one) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

pp: case op.op.one.zero
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

pp: case op.op.one.one
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
<;>

Goal state after:
case op.op.zero.zero
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.zero.one
f : op zero ⟶ op one
g : unop (op one) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.one.zero
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.one.one
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op.zero.zero.id
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))

pp: case op.op.one.zero.left
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op left)

pp: case op.op.one.zero.right
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op right)

pp: case op.op.one.one.id
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))

Tactic:
<;>

Goal state after:
case op.op.zero.zero.id
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))

case op.op.one.zero.left
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op left)

case op.op.one.zero.right
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op right)

case op.op.one.one.id
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app zero) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj zero) =
    𝟙 (walkingParallelPairOp.obj zero)

pp: case one
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app one) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj one) =
    𝟙 (walkingParallelPairOp.obj one)

Tactic:
<;>

Goal state after:
case zero
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app zero) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj zero) =
    𝟙 (walkingParallelPairOp.obj zero)

case one
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app one) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj one) =
    𝟙 (walkingParallelPairOp.obj one)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (left ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g left ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

pp: case right.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (right ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g right ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

pp: case id.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ left) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g left

pp: case id.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ right) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g right

pp: case id.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
X✝ : WalkingParallelPair
⊢ parallelPairHom f g (WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝) =
    parallelPairHom f g (WalkingParallelPairHom.id X✝) ≫ parallelPairHom f g (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (left ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g left ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

case right.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (right ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g right ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

case id.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ left) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g left

case id.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ right) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g right

case id.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
X✝ : WalkingParallelPair
⊢ parallelPairHom f g (WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝) =
    parallelPairHom f g (WalkingParallelPairHom.id X✝) ≫ parallelPairHom f g (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj zero = F.obj zero

pp: case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj one = F.obj one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj zero = F.obj zero

case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj one = F.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.obj zero = (parallelPair (F.map left) (F.map right)).obj zero

pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.obj one = (parallelPair (F.map left) (F.map right)).obj one

Tactic:
<;>

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.obj zero = (parallelPair (F.map left) (F.map right)).obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.obj one = (parallelPair (F.map left) (F.map right)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map left ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map right ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map left ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map right ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inl f f ≫ (pushoutSymmetry f f).hom = pushout.inl f f ≫ 𝟙 (pushout f f)

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inr f f ≫ (pushoutSymmetry f f).hom = pushout.inr f f ≫ 𝟙 (pushout f f)

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inl f f ≫ (pushoutSymmetry f f).hom = pushout.inl f f ≫ 𝟙 (pushout f f)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inr f f ≫ (pushoutSymmetry f f).hom = pushout.inr f f ≫ 𝟙 (pushout f f)
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))

pp: case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))

Tactic:
<;>

Goal state after:
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))

case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))

pp: case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))

Tactic:
<;>

Goal state after:
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))

case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
C : Type u
X Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y✝
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
Y : WalkingParallelPair
f : zero ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (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

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

Tactic:
<;>

Goal state after:
case zero
C : Type u
X Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y✝
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
Y : WalkingParallelPair
f : zero ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (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

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