Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

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

pp: case zero.one.left
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 left ≫
      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) ⋯ =
    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 left

pp: case zero.one.right
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 right ≫
      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) ⋯ =
    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 right

pp: case one.one.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 one) ≫
      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) ⋯ =
    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 (WalkingParallelPairHom.id one)

Tactic:
<;>

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)

case zero.one.left
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 left ≫
      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) ⋯ =
    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 left

case zero.one.right
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 right ≫
      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) ⋯ =
    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 right

case one.one.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 one) ≫
      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) ⋯ =
    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 (WalkingParallelPairHom.id one)