awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f_1 j₁ ≫ π = f_1 j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
id :
  Eq (α :=
    (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
    ((parallelFamily f_1).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i)))
line :
  ∀ (k : J),
    Eq (α :=
      (parallelFamily f_1).obj zero ⟶
        Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) P) one)
      ((parallelFamily f_1).map (Hom.line k) ≫
        WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
          (parallelFamily f_1).obj x ⟶
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
          one (f_1 (Classical.arbitrary J) ≫ π) π)
      (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) P) zero)
        (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
          (parallelFamily f_1).obj x ⟶
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
          zero (f_1 (Classical.arbitrary J) ≫ π) π)
        (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.line k)))
⊢ Eq (α :=
    (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) j)
    ((parallelFamily f_1).map f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        j (f_1 (Classical.arbitrary J) ≫ π) π)
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) 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
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
i : WalkingParallelFamily J
⊢ Eq (α :=
    (parallelFamily f).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
    ((parallelFamily f).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f (Classical.arbitrary J) ≫ π) π)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f (Classical.arbitrary J) ≫ π) π)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (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
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ Eq (α :=
    (parallelFamily f).obj zero ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        one)
    ((parallelFamily f).map (line k) ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        one (f (Classical.arbitrary J) ≫ π) π)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        zero)
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        zero (f (Classical.arbitrary J) ≫ π) π)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (line k)))

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

Premises used: Classical.arbitrary
-- 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₂
⊢ (ofι ι w).ι = ι

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)
inst_1 : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
⊢ (ofπ π w).π = π

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₂ : J
t : Trident f
rw : t.π.app one = t.ι ≫ f j₂
rw₁ rw₂ :
  Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt)
        zero ⟶
      Y)
    (t.π.app one :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) one ⟶
        (parallelFamily f).obj one)
    (t.π.app one)
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂

Tactic:
rw [t.app_zero, t.app_zero]

Premises used: CategoryTheory.Limits.Trident.app_zero
-- 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₂ : J
t : Cotrident f
rw : t.ι.app zero = f j₂ ≫ t.π
rw₁ rw₂ :
  Eq (α :=
    X ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) one)
    (t.ι.app zero :
      (parallelFamily f).obj zero ⟶
        Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) zero)
    (t.ι.app zero)
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π

Tactic:
rw [t.app_one, t.app_one]

Premises used: CategoryTheory.Limits.Cotrident.app_one
-- 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
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
rw :
  Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app zero ≫ f (Classical.arbitrary J))
    (l ≫ s.π.app zero ≫ f (Classical.arbitrary J))
rw₁ rw₂ : l ≫ s.ι ≫ f (Classical.arbitrary J) = l ≫ s.π.app zero ≫ f (Classical.arbitrary J)
⊢ Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app one) (l ≫ s.π.app one)

Tactic:
rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]

Premises used: CategoryTheory.Limits.Trident.app_zero, Classical.arbitrary
-- 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
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
rw : (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
rw₁ : f (Classical.arbitrary J) ≫ s.ι.app one ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
rw₂ :
  Eq.{v + 1} (α := (parallelFamily f).obj zero ⟶ W) (f (Classical.arbitrary J) ≫ s.ι.app one ≫ k)
    (f (Classical.arbitrary J) ≫ s.ι.app one ≫ l)
rw₃ rw₄ : f (Classical.arbitrary J) ≫ s.π ≫ l = f (Classical.arbitrary J) ≫ s.ι.app one ≫ l
⊢ Eq (α := (parallelFamily f).obj zero ⟶ W) (s.ι.app zero ≫ k) (s.ι.app zero ≫ l)

Tactic:
rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cotrident.app_one, Classical.arbitrary
-- 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
s : Trident f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k = l

Tactic:
hs.hom_ext <| Trident.equalizer_ext _ h

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.Trident.equalizer_ext
-- 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
s : Cotrident f
hs : IsColimit s
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ k = l

Tactic:
hs.hom_ext <| Cotrident.coequalizer_ext _ h

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cotrident.coequalizer_ext
-- 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
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
rw : lift s ≫ t.π.app zero ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
rw₁ : ι s ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
rw₂ rw₃ : Eq (α := s.pt ⟶ (parallelFamily f).obj one) (s.π.app one) (s.π.app one)
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj one) (lift s ≫ t.π.app one) (s.π.app one)

Tactic:
rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]

Premises used: CategoryTheory.Limits.WalkingParallelFamily.Hom.line, CategoryTheory.Limits.Cone.w, Classical.arbitrary
-- 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
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
rw : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ t.ι.app one ≫ desc s = s.ι.app zero
rw₁ : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ π s = s.ι.app zero
rw₂ rw₃ : Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (s.ι.app zero) (s.ι.app zero)
⊢ Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (t.ι.app zero ≫ desc s) (s.ι.app zero)

Tactic:
rw [← t.w_assoc (line (Classical.arbitrary J)), fac, s.w]

Premises used: CategoryTheory.Limits.Cocone.w_assoc, CategoryTheory.Limits.WalkingParallelFamily.Hom.line, CategoryTheory.Limits.Cocone.w, Classical.arbitrary
-- 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
t : Trident f
ht : IsLimit t
Z : C
k : Z ⟶ t.pt
⊢ ∀ (j₁ j₂ : J), (k ≫ t.ι) ≫ f j₁ = (k ≫ t.ι) ≫ f j₂

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
t : Trident f
ht : IsLimit t
Z Z' : C
q : Z' ⟶ Z
k : Z ⟶ t.pt
⊢ Eq (α := Z' ⟶ X)
    (↑((homIso ht Z' : (a : Z' ⟶ t.pt) → { h : Z' ⟶ X // ∀ (j₁ j₂ : J), h ≫ f j₁ = h ≫ f j₂ }) (q ≫ k)) : Z' ⟶ X)
    (q ≫ (↑((homIso ht Z : (a : Z ⟶ t.pt) → { h : Z ⟶ X // ∀ (j₁ j₂ : J), h ≫ f j₁ = h ≫ f j₂ }) k) : Z ⟶ X))

Tactic:
Category.assoc _ _ _

Premises used: CategoryTheory.Category.assoc
-- 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
t : Cotrident f
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ ∀ (j₁ j₂ : J), f j₁ ≫ t.π ≫ k = f j₂ ≫ t.π ≫ k

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
t : Cotrident f
Z Z' : C
q : Z ⟶ Z'
ht : IsColimit t
k : t.pt ⟶ Z
⊢ Eq (α := Y ⟶ Z')
    (↑((homIso ht Z' : (a : t.pt ⟶ Z') → { h : Y ⟶ Z' // ∀ (j₁ j₂ : J), f j₁ ≫ h = f j₂ ≫ h }) (k ≫ q)) : Y ⟶ Z')
    ((↑((homIso ht Z : (a : t.pt ⟶ Z) → { h : Y ⟶ Z // ∀ (j₁ j₂ : J), f j₁ ≫ h = f j₂ ≫ h }) k) : Y ⟶ Z) ≫ q)

Tactic:
(Category.assoc _ _ _).symm

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t :
  Trident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one)
    fun (j : J) ↦ F.map (line j)
X : WalkingParallelFamily J
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 =
    F.obj WalkingParallelFamily.zero
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 WalkingParallelFamily.one
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      X =
    F.obj 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
zero zero₁ zero₂ 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 =
    F.obj 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
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j)
one one₁ one₂ 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 =
    F.obj WalkingParallelFamily.one

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
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (Hom.line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
id :
  Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)
line :
  ∀ (a : J),
    Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.line a) ≫ t.π.app one ≫ eqToHom ⋯ =
      (t.π.app zero ≫ eqToHom ⋯) ≫ F.map (Hom.line a)
⊢ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g

Tactic:
cases g
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t :
  Cotrident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one)
    fun (j : J) ↦ F.map (line j)
X : 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 X =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
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
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j)
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 Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (Hom.line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
id :
  F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j)
line :
  ∀ (a : J),
    F.map (Hom.line a) ≫ eqToHom ⋯ ≫ t.ι.app one =
      (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.line a)
⊢ F.map g ≫ eqToHom ⋯ ≫ t.ι.app j' =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g

Tactic:
cases g
-- 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
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j)

Tactic:
simp [Cotrident.app_one t]

Premises used: CategoryTheory.Limits.Cotrident.app_one
-- 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
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
a : J
⊢ F.map (line a) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (line a)

Tactic:
simp [Cotrident.app_one t]

Premises used: CategoryTheory.Limits.Cotrident.app_one
-- 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
t :
  Trident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one)
    fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
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 =
    F.obj WalkingParallelFamily.zero
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 WalkingParallelFamily.one
⊢ 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 =
    F.obj j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ (ofTrident t).π.app j = t.π.app j ≫ eqToHom ⋯

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
t :
  Cotrident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one)
    fun (j : J) ↦ F.map (line j)
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