awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
⊢ t.ι.app one = t.π

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ f
rw₁ : s.π.app zero ≫ (parallelPair f g).map left = s.π.app zero ≫ f
rw₂ rw₃ : s.π.app zero ≫ f = s.π.app zero ≫ f
⊢ s.π.app one = s.ι ≫ f

Tactic:
rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]

Premises used: CategoryTheory.Limits.parallelPair_map_left, CategoryTheory.Limits.Fork.app_zero_eq_ι, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ g
rw₁ : s.π.app zero ≫ (parallelPair f g).map right = s.π.app zero ≫ g
rw₂ rw₃ : s.π.app zero ≫ g = s.π.app zero ≫ g
⊢ s.π.app one = s.ι ≫ g

Tactic:
rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]

Premises used: CategoryTheory.Limits.Fork.app_zero_eq_ι, CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.Limits.parallelPair_map_right, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = f ≫ s.ι.app one
rw₁ : (parallelPair f g).map left ≫ s.ι.app one = f ≫ s.ι.app one
rw₂ rw₃ : f ≫ s.ι.app one = f ≫ s.ι.app one
⊢ s.ι.app zero = f ≫ s.π

Tactic:
rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]

Premises used: CategoryTheory.Limits.parallelPair_map_left, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingParallelPairHom.left, CategoryTheory.Limits.Cofork.app_one_eq_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = g ≫ s.ι.app one
rw₁ : (parallelPair f g).map right ≫ s.ι.app one = g ≫ s.ι.app one
rw₂ rw₃ : g ≫ s.ι.app one = g ≫ s.ι.app one
⊢ s.ι.app zero = g ≫ s.π

Tactic:
rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.Limits.parallelPair_map_right, CategoryTheory.Limits.Cofork.app_one_eq_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
P : C
ι : P ⟶ X_1
w : ι ≫ f = ι ≫ g
X : WalkingParallelPair
zero :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.zero ⟶
    (parallelPair f g).obj WalkingParallelPair.zero
one :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.one ⟶
    (parallelPair f g).obj WalkingParallelPair.one
⊢ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f g).obj X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶ (parallelPair f g).obj zero

Tactic:
exact ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one

Tactic:
exact ι ≫ f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f_1 = ι ≫ g
f : one ⟶ zero
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f_1 g).obj zero)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : zero = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶
            (parallelPair f_1 g).obj zero)
        zero
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f_1 g).obj X_1)
            ι ⋯)
        (fun (h : zero = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f_1 g).obj X_1)
            (ι ≫ f_1) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : one = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶
            (parallelPair f_1 g).obj one)
        one
        (fun (h : one = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f_1 g).obj X_1)
            ι ⋯)
        (fun (h : one = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f_1 g).obj X_1)
            (ι ≫ f_1) ⋯)
        ⋯ ≫
      (parallelPair f_1 g).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶ (parallelPair f g).obj zero)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) (WalkingParallelPairHom.id zero) ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : zero = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶
            (parallelPair f g).obj zero)
        zero
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : zero = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : zero = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶
            (parallelPair f g).obj zero)
        zero
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : zero = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id zero))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶ (parallelPair f g).obj one)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) left ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : one = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one)
        one
        (fun (h : one = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : one = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : zero = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶
            (parallelPair f g).obj zero)
        zero
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : zero = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯ ≫
      (parallelPair f g).map left)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶ (parallelPair f g).obj one)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) right ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : one = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one)
        one
        (fun (h : one = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : one = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : zero = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶
            (parallelPair f g).obj zero)
        zero
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : zero = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯ ≫
      (parallelPair f g).map right)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) (WalkingParallelPairHom.id one) ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : one = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one)
        one
        (fun (h : one = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : one = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : one = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one)
        one
        (fun (h : one = zero) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            ι ⋯)
        (fun (h : one = one) ↦
          Eq.ndrec (motive := fun (X_1 : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X_1 ⟶
              (parallelPair f g).obj X_1)
            (ι ≫ f) ⋯)
        ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id one))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
P : C
π : Y ⟶ P
w : f_1 ≫ π = g ≫ π
i j : WalkingParallelPair
f : i ⟶ j
left :
  Eq (α :=
    (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f_1 g).map WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x)
        zero (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPairHom.left)
right :
  Eq (α :=
    (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f_1 g).map WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x)
        zero (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPairHom.right)
id :
  Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) i)
    ((parallelPair f_1 g).map (WalkingParallelPairHom.id i) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) (WalkingParallelPairHom.id i))
⊢ Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) j)
    ((parallelPair f_1 g).map f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) j
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ Eq (α :=
    (parallelPair f g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f g).map left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) zero
        (f ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) left)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ Eq (α :=
    (parallelPair f g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f g).map right ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) zero
        (f ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) right)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
i : WalkingParallelPair
⊢ Eq (α := (parallelPair f g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) i)
    ((parallelPair f g).map (WalkingParallelPairHom.id i) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) (WalkingParallelPairHom.id i))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ (ofι ι w).ι = ι

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (ofπ π w).π = π

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
rw : t.π.app one = t.ι ≫ g
rw₁ rw₂ : t.π.app one = t.π.app one
⊢ t.ι ≫ f = t.ι ≫ g

Tactic:
rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]

Premises used: CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left, CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
rw : t.ι.app zero = g ≫ t.π
rw₁ rw₂ : t.ι.app zero = t.ι.app zero
⊢ f ≫ t.π = g ≫ t.π

Tactic:
rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]

Premises used: CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left, CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
simp : (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f
⊢ k ≫ s.ι ≫ f = l ≫ s.ι ≫ f

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f

Tactic:
congrArg (· ≫ f) h

Premises used: congrArg, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f

Tactic:
exact congrArg (· ≫ f) h

Premises used: congrArg, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.ι ≫ f = l ≫ s.ι ≫ f

Tactic:
have : k ≫ ι s ≫ f = l ≫ ι s ≫ f := by
      simp only [← Category.assoc]; exact congrArg (· ≫ f) h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
rw : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
rw₁ rw₂ : l ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
rw [s.app_one_eq_ι_comp_left, this]

Premises used: CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l

Tactic:
simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
hs : IsLimit s
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k = l

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

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.Fork.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
hs : IsColimit s
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ k = l

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

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cofork.coequalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Fork f g
hs : IsLimit s
⊢ hs.lift t ≫ s.ι = t.ι

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Cofork f g
hs : IsColimit s
⊢ s.π ≫ hs.desc t = t.π

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
hs : IsLimit s
W : C
k : W ⟶ X
h : k ≫ f = k ≫ g
⊢ lift hs k h ≫ s.ι = k

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
hs : IsLimit s
W : C
k : W ⟶ X
h : k ≫ f = k ≫ g
⊢ lift hs k h ≫ s.ι = k

Tactic:
simp