Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }) =
    { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }

pp: case zero.line
J : Type w
a✝ : J
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := one, hom := line a✝ }) =
    { left := zero, right := one, hom := line a✝ }

pp: case one.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }) =
    { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }

Tactic:
<;>

Goal state after:
case zero.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }) =
    { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }

case zero.line
J : Type w
a✝ : J
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := one, hom := line a✝ }) =
    { left := zero, right := one, hom := line a✝ }

case one.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }) =
    { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }