Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily J
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

pp: case id.line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, Hom.id zero ≫ line a✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, zero, Hom.id zero with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

pp: case line.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, line a✝ ≫ Hom.id one with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match one, one, Hom.id one with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
<;>

Goal state after:
case id.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily J
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

case id.line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, Hom.id zero ≫ line a✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, zero, Hom.id zero with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

case line.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, line a✝ ≫ Hom.id one with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match one, one, Hom.id one with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j