awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasInitial.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ IsIso (X := F.obj (initial.{v, u} J)) (Y := colimit F) (colimit.ι F (initial.{v, u} J))

Tactic:
isIso_ι_of_isInitial initialIsInitial F

Premises used: CategoryTheory.Limits.isIso_ι_of_isInitial, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
t : Eq.{w + 1} (α := WalkingParallelFamily J) zero one
⊢ False

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
t : Eq.{w + 1} (α := WalkingParallelFamily J) one zero
⊢ False

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
X : WalkingParallelFamily J
⊢ Hom.id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Arrow (WalkingParallelFamily J))
    ((fun (x : Option (Option J)) ↦
        (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
          | none => Arrow.mk (X := zero) (𝟙 zero)
          | some none => Arrow.mk (X := one) (𝟙 one)
          | some (some t) => Arrow.mk (line t) :
          Arrow (WalkingParallelFamily J)))
      ((fun (f : Arrow (WalkingParallelFamily J)) ↦
          (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
            Option (Option J)))
        { left := zero, right := zero, hom := Hom.id (Functor.obj (𝟭 (WalkingParallelFamily J)) zero) }))
    { left := zero, right := zero, hom := Hom.id (Functor.obj (𝟭 (WalkingParallelFamily J)) zero) }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
a : J
⊢ Eq.{w + 1} (α := Arrow (WalkingParallelFamily J))
    ((fun (x : Option (Option J)) ↦
        (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
          | none => Arrow.mk (X := zero) (𝟙 zero)
          | some none => Arrow.mk (X := one) (𝟙 one)
          | some (some t) => Arrow.mk (line t) :
          Arrow (WalkingParallelFamily J)))
      ((fun (f : Arrow (WalkingParallelFamily J)) ↦
          (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
            Option (Option J)))
        { left := zero, right := one, hom := line a }))
    { left := zero, right := one, hom := line a }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Arrow (WalkingParallelFamily J))
    ((fun (x : Option (Option J)) ↦
        (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
          | none => Arrow.mk (X := zero) (𝟙 zero)
          | some none => Arrow.mk (X := one) (𝟙 one)
          | some (some t) => Arrow.mk (line t) :
          Arrow (WalkingParallelFamily J)))
      ((fun (f : Arrow (WalkingParallelFamily J)) ↦
          (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
            Option (Option J)))
        { left := one, right := one, hom := Hom.id (Functor.obj (𝟭 (WalkingParallelFamily J)) one) }))
    { left := one, right := one, hom := Hom.id (Functor.obj (𝟭 (WalkingParallelFamily J)) one) }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Option (Option J))
    ((fun (f : Arrow (WalkingParallelFamily J)) ↦
        (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
          Option (Option J)))
      ((fun (x : Option (Option J)) ↦
          (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
            | none => Arrow.mk (X := zero) (𝟙 zero)
            | some none => Arrow.mk (X := one) (𝟙 one)
            | some (some t) => Arrow.mk (line t) :
            Arrow (WalkingParallelFamily J)))
        none))
    none

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Option (Option J))
    ((fun (f : Arrow (WalkingParallelFamily J)) ↦
        (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
          Option (Option J)))
      ((fun (x : Option (Option J)) ↦
          (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
            | none => Arrow.mk (X := zero) (𝟙 zero)
            | some none => Arrow.mk (X := one) (𝟙 one)
            | some (some t) => Arrow.mk (line t) :
            Arrow (WalkingParallelFamily J)))
        (some none)))
    (some none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
val : J
⊢ (fun (f : Arrow (WalkingParallelFamily J)) ↦
        (match (motive := (x x_1 : WalkingParallelFamily J) → (x ⟶ x_1) → Option (Option J)) 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) :
          Option (Option J)))
      ((fun (x : Option (Option J)) ↦
          (match (motive := Option (Option J) → Arrow (WalkingParallelFamily J)) x with
            | none => Arrow.mk (X := zero) (𝟙 zero)
            | some none => Arrow.mk (X := one) (𝟙 one)
            | some (some t) => Arrow.mk (line t) :
            Arrow (WalkingParallelFamily J)))
        (some (some val))) =
    some (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily f).obj zero = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily f).obj one = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j : J
⊢ (parallelFamily f).map (line j) = f j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
j : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.zero
one :
  F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.one
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
zero zero₁ zero₂ zero₃ :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
one one₁ one₂ one₃ :
  F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one
⊢ F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
zero :
  Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
    (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) WalkingParallelFamily.zero)
    (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      WalkingParallelFamily.zero)
one :
  Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
    (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) WalkingParallelFamily.one)
    (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      WalkingParallelFamily.one)
⊢ Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) X =
    Functor.obj
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
    (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) zero)
    (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      zero)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
    (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) one)
    (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      one)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelPair
zero :
  Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      WalkingParallelPair.zero =
    Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero
one :
  Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      WalkingParallelPair.one =
    Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one
⊢ Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      X =
    Functor.obj (𝟭 WalkingParallelPair) X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      WalkingParallelPair.zero =
    Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      WalkingParallelPair.one =
    Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
t : Trident f
⊢ t.ι = t.π.app zero

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
t : Cotrident f
⊢ t.π = t.ι.app one

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
rw : s.π.app zero ≫ f j = s.π.app zero ≫ (parallelFamily f).map (line j)
rw₁ rw₂ :
  Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
        zero ⟶
      Y)
    (s.π.app zero ≫ f j) (s.π.app zero ≫ f j)
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
        zero ⟶
      Y)
    (s.π.app zero ≫ f j :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) zero ⟶
        Y)
    (s.π.app one :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one ⟶
        (parallelFamily f).obj one)

Tactic:
rw [← s.w (line j), parallelFamily_map_left]

Premises used: CategoryTheory.Limits.WalkingParallelFamily.Hom.line, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.parallelFamily_map_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
rw : f j ≫ s.ι.app one = (parallelFamily f).map (line j) ≫ s.ι.app one
rw₁ rw₂ :
  Eq.{v + 1} (α :=
    X ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one)
    (f j ≫ s.ι.app one) (f j ≫ s.ι.app one)
⊢ Eq.{v + 1} (α :=
    X ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one)
    (f j ≫ s.ι.app one) (s.ι.app zero)

Tactic:
rw [← s.w (line j), parallelFamily_map_left]

Premises used: CategoryTheory.Limits.WalkingParallelFamily.Hom.line, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.parallelFamily_map_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f_1 j₁ = ι ≫ f_1 j₂
i j : WalkingParallelFamily J
f : i ⟶ j
id :
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj i)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J))))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map (Hom.id i))
line :
  ∀ (k : J),
    Eq.{v + 1} (α :=
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
          zero ⟶
        (parallelFamily f_1).obj one)
      (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) P) one)
        (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.line k))
        (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
            (parallelFamily f_1).obj x)
          one ι (ι ≫ f_1 (Classical.arbitrary J))))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
            (parallelFamily f_1).obj x)
          zero ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
        (parallelFamily f_1).map (Hom.line k))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj j)
    (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        j ι (ι ≫ f_1 (Classical.arbitrary J)))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map f)

Tactic:
obtain - | k := f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
i : WalkingParallelFamily J
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f).obj i)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f).obj x)
        i ι (ι ≫ f (Classical.arbitrary J))))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f).obj x)
        i ι (ι ≫ f (Classical.arbitrary J)) ≫
      (parallelFamily f).map (Hom.id i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
k : J
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        zero ⟶
      (parallelFamily f).obj one)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        one)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (line k))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f).obj x)
        one ι (ι ≫ f (Classical.arbitrary J))))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f).obj x)
        zero ι (ι ≫ f (Classical.arbitrary J)) ≫
      (parallelFamily f).map (line k))

Tactic:
simp [w (Classical.arbitrary J) k]

Premises used: Classical.arbitrary