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
s : Cofork f g
hs : IsColimit s
W : C
k : Y ⟶ W
h : f ≫ k = g ≫ k
⊢ s.π ≫ desc hs k h = k

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cofork.IsColimit.desc, 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 : Cofork f g
hs : IsColimit s
W : C
k : Y ⟶ W
h : f ≫ k = g ≫ k
⊢ s.π ≫ desc hs k h = k

Tactic:
simp
-- 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
⊢ ∃! l : W ⟶ s.pt, l ≫ s.ι = k

Tactic:
⟨hs.lift <| Fork.ofι _ h, hs.fac _ _, fun _ hm =>
    Fork.IsLimit.hom_ext hs <| hm.symm ▸ (hs.fac (Fork.ofι _ h) WalkingParallelPair.zero).symm⟩

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.IsLimit.hom_ext, Eq.rec, ExistsUnique, And.intro, Exists.intro, Eq.symm, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.Limits.WalkingParallelPair.zero, 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 : Cofork f g
hs : IsColimit s
W : C
k : Y ⟶ W
h : f ≫ k = g ≫ k
⊢ ∃! d : s.pt ⟶ W, s.π ≫ d = k

Tactic:
⟨hs.desc <| Cofork.ofπ _ h, hs.fac _ _, fun _ hm =>
    Cofork.IsColimit.hom_ext hs <| hm.symm ▸ (hs.fac (Cofork.ofπ _ h) WalkingParallelPair.one).symm⟩

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingParallelPair.one, Eq.rec, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.IsColimit.desc, ExistsUnique, And.intro, Exists.intro, Eq.symm
-- 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
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
simp [← Category.assoc, fac]

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
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
m : s.pt ⟶ t.pt
j : ∀ (j : WalkingParallelPair), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
aesop
-- 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
desc : (s : Cofork f g) → t.pt ⟶ s.pt
fac : ∀ (s : Cofork f g), t.π ≫ desc s = s.π
uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt), t.π ≫ m = s.π → m = desc s
s : Cocone (parallelPair f g)
j : WalkingParallelPair
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

Tactic:
simp_all
-- 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
desc : (s : Cofork f g) → t.pt ⟶ s.pt
fac : ∀ (s : Cofork f g), t.π ≫ desc s = s.π
uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt), t.π ≫ m = s.π → m = desc s
⊢ ∀ (s : Cocone (parallelPair f g)) (m : t.pt ⟶ s.pt),
    (∀ (j : WalkingParallelPair), t.ι.app j ≫ m = s.ι.app j) → m = desc s

Tactic:
aesop
-- 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
hs : ∀ (s : Fork f g), ∃! l : s.pt ⟶ t.pt, l ≫ t.ι = s.ι
choose :
  (d : (s : Fork f g) → s.pt ⟶ t.pt) →
    (hd : ∀ (s : Fork f g), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) (d s)) →
      (hd' : ∀ (s : Fork f g) (y : s.pt ⟶ t.pt), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) y → y = d s) → IsLimit t
⊢ IsLimit t

Tactic:
choose d hd hd' using hs
-- 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
d : (s : Fork f g) → s.pt ⟶ t.pt
hd : ∀ (s : Fork f g), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) (d s)
hd' : ∀ (s : Fork f g) (y : s.pt ⟶ t.pt), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) y → y = d s
⊢ IsLimit t

Tactic:
exact Fork.IsLimit.mk _ d hd fun s m hm => hd' _ _ hm

Premises used: CategoryTheory.Limits.Fork.IsLimit.mk
-- 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
hs : ∀ (s : Cofork f g), ∃! d : t.pt ⟶ s.pt, t.π ≫ d = s.π
choose :
  (d : (s : Cofork f g) → t.pt ⟶ s.pt) →
    (hd : ∀ (s : Cofork f g), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) (d s)) →
      (hd' : ∀ (s : Cofork f g) (y : t.pt ⟶ s.pt), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) y → y = d s) → IsColimit t
⊢ IsColimit t

Tactic:
choose d hd hd' using hs
-- 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
d : (s : Cofork f g) → t.pt ⟶ s.pt
hd : ∀ (s : Cofork f g), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) (d s)
hd' : ∀ (s : Cofork f g) (y : t.pt ⟶ s.pt), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) y → y = d s
⊢ IsColimit t

Tactic:
exact Cofork.IsColimit.mk _ d hd fun s m hm => hd' _ _ hm

Premises used: CategoryTheory.Limits.Cofork.IsColimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
X Y : C
f g : X ⟶ Y
t : Fork f g
ht : IsLimit t
Z : C
k : Z ⟶ t.pt
⊢ (k ≫ t.ι) ≫ f = (k ≫ t.ι) ≫ g

Tactic:
simp only [Category.assoc, t.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.condition
-- 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
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 // h ≫ f = h ≫ g }) (q ≫ k)) : Z' ⟶ X)
    (q ≫ (↑((homIso ht Z : (a : Z ⟶ t.pt) → { h : Z ⟶ X // h ≫ f = h ≫ g }) k) : Z ⟶ X))

Tactic:
Category.assoc _ _ _

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
X Y : C
f g : X ⟶ Y
t : Cofork f g
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ f ≫ t.π ≫ k = g ≫ t.π ≫ k

Tactic:
simp only [← Category.assoc, t.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition
-- 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
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' // f ≫ h = g ≫ h }) (k ≫ q)) : Y ⟶ Z')
    ((↑((homIso ht Z : (a : t.pt ⟶ Z) → { h : Y ⟶ Z // f ≫ h = g ≫ h }) k) : Y ⟶ Z) ≫ q)

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

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
X : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj X = F.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map left

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map right

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
X_1 : WalkingParallelPair
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) (WalkingParallelPairHom.id X_1) ≫
      t.π.app X_1 ≫ eqToHom ⋯ =
    (t.π.app X_1 ≫ eqToHom ⋯) ≫ F.map (WalkingParallelPairHom.id X_1)

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
X : WalkingParallelPair
⊢ F.obj X = (parallelPair (F.map left) (F.map right)).obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
⊢ F.map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) left

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
⊢ F.map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) right

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
X_1 : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X_1) ≫ eqToHom ⋯ ≫ t.ι.app X_1 =
    (eqToHom ⋯ ≫ t.ι.app X_1) ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) (WalkingParallelPairHom.id X_1)

Tactic:
simp [t.condition]

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Fork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ (ofFork t).π.app j = t.π.app j ≫ eqToHom ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cofork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ (ofCofork t).ι.app j = eqToHom ⋯ ≫ t.ι.app j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
X : WalkingParallelPair
⊢ F.obj X = (parallelPair (F.map left) (F.map right)).obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
X_1 : WalkingParallelPair
⊢ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) (WalkingParallelPairHom.id X_1) ≫
      t.π.app X_1 ≫ eqToHom ⋯ =
    (t.π.app X_1 ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
X : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj X = F.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
X_1 : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X_1) ≫ eqToHom ⋯ ≫ t.ι.app X_1 =
    (eqToHom ⋯ ≫ t.ι.app X_1) ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) t.pt) (WalkingParallelPairHom.id X_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cone F
j : WalkingParallelPair
⊢ (ofCone t).π.app j = t.π.app j ≫ eqToHom ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
t : Cocone F
j : WalkingParallelPair
⊢ (ofCocone t).ι.app j = eqToHom ⋯ ≫ t.ι.app j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g f' g' : X ⟶ Y
α : parallelPair f g ⟶ parallelPair f' g'
c : Fork f g
⊢ ι ((Cone.postcompose α).obj c) = c.ι ≫ α.app zero

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 f' g' : X ⟶ Y
α : parallelPair f g ⟶ parallelPair f' g'
c : Cofork f' g'
⊢ π ((Cocone.precompose α).obj c) = α.app one ≫ c.π

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 t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app zero = s.π.app zero

Tactic:
w

Premises used: CategoryTheory.Limits.Fork.ι
-- 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
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app zero = s.π.app zero

Tactic:
exact w
-- 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
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
one : (k ≫ t.ι) ≫ f = s.ι ≫ f
⊢ k ≫ t.π.app WalkingParallelPair.one = s.π.app WalkingParallelPair.one

Tactic:
simp only [Fork.app_one_eq_ι_comp_left, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, 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 t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ (k ≫ t.ι) ≫ f = s.ι ≫ f

Tactic:
congr
-- 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
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
rw : i.inv ≫ i.hom ≫ t.ι = t.ι
rw₁ rw₂ : t.ι = t.ι
⊢ i.inv ≫ s.ι = t.ι

Tactic:
rw [← w, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc
-- 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
w' : ι' ≫ f = ι' ≫ g
h : ι = ι'
⊢ Iso.hom (Iso.refl (Fork.ofι ι w).pt) ≫ (Fork.ofι ι' w').ι = (Fork.ofι ι w).ι

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map left ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map left

Tactic:
simp [comm₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map right ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map right

Tactic:
simp [comm₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
c : Fork f g
⊢ ((equivOfIsos e₀ e₁ comm₁ comm₂).functor.obj c).ι = c.ι ≫ e₀.hom

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
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
c : Fork f' g'
⊢ ((equivOfIsos e₀ e₁ comm₁ comm₂).inverse.obj c).ι = c.ι ≫ e₀.inv

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
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero

Tactic:
simp [Cofork.app_zero_eq_comp_π_left, w]

Premises used: 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 t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
w

Premises used: 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 t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
s t : Fork f_1 g
f : s ⟶ t
mk :
  ∀ (pt : C) (π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g)
    (f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ t), f.hom ≫ t.ι = ι { pt := pt, π := π }
⊢ f.hom ≫ t.ι = s.ι

Tactic:
cases s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
t : Fork f_1 g
pt : C
π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g
f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ t
mk :
  ∀ (pt_1 : C) (π_1 : Functor.obj (Functor.const WalkingParallelPair) pt_1 ⟶ parallelPair f_1 g)
    (f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ { pt := pt_1, π := π_1 }),
    f.hom ≫ ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } = ι { pt := pt, π := π }
⊢ f.hom ≫ t.ι = ι { pt := pt, π := π }

Tactic:
cases t
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
pt : C
π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g
pt_1 : C
π_1 : Functor.obj (Functor.const WalkingParallelPair) pt_1 ⟶ parallelPair f_1 g
f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ { pt := pt_1, π := π_1 }
mk :
  ∀
    (hom :
      { pt := pt, π := π : Cone (parallelPair f_1 g) }.pt ⟶ { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) }.pt)
    (w :
      ∀ (j : WalkingParallelPair),
        hom ≫ { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) }.π.app j = { pt := pt, π := π }.π.app j),
    { hom := hom, w := w :
            ConeMorphism { pt := pt, π := π : Cone (parallelPair f_1 g) }
              { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } }.hom ≫
        ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } =
      ι { pt := pt, π := π }
⊢ f.hom ≫ ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } = ι { pt := pt, π := π }

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
pt : C
π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f g
pt_1 : C
π_1 : Functor.obj (Functor.const WalkingParallelPair) pt_1 ⟶ parallelPair f g
hom : { pt := pt, π := π : Cone (parallelPair f g) }.pt ⟶ { pt := pt_1, π := π_1 : Cone (parallelPair f g) }.pt
w :
  ∀ (j : WalkingParallelPair),
    hom ≫ { pt := pt_1, π := π_1 : Cone (parallelPair f g) }.π.app j = { pt := pt, π := π }.π.app j
⊢ { hom := hom, w := w :
          ConeMorphism { pt := pt, π := π : Cone (parallelPair f g) }
            { pt := pt_1, π := π_1 : Cone (parallelPair f g) } }.hom ≫
      ι { pt := pt_1, π := π_1 : Cone (parallelPair f g) } =
    ι { pt := pt, π := π }

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
s t : Cofork f_1 g
f : s ⟶ t
mk :
  ∀ (pt : C) (ι : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt)
    (f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ t),
    Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = t.π
⊢ s.π ≫ f.hom = t.π

Tactic:
cases s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
t : Cofork f_1 g
pt : C
ι : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt
f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ t
mk :
  ∀ (pt_1 : C) (ι_1 : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt_1)
    (f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ { pt := pt_1, ι := ι_1 }),
    Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = Cofork.π { pt := pt_1, ι := ι_1 }
⊢ Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = t.π

Tactic:
cases t