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

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

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

Tactic:
rw [Iso.comp_inv_eq, w]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- 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 ≫ π
w' : f ≫ π' = g ≫ π'
h : π = π'
⊢ (Cofork.ofπ π w).π ≫ Iso.hom (Iso.refl (Cofork.ofπ π w).pt) = (Cofork.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
c : Cofork f g
f' g' : X' ⟶ Y'
c' : Cofork f' g'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
e : c.pt ≅ c'.pt
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
comm₃ : e₁.inv ≫ c.π ≫ e.hom = c'.π
i : parallelPair f g ≅ parallelPair f' g' := parallelPair.ext e₀ e₁ ⋯ ⋯
rw : π ((Cocone.precompose i.inv).obj c) ≫ e.hom = (e₁.inv ≫ c.π) ≫ e.hom
⊢ π ((Cocone.precompose i.inv).obj c) ≫ e.hom = c'.π

Tactic:
rw [← comm₃, ← 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
X' Y' : C
c : Cofork f g
f' g' : X' ⟶ Y'
c' : Cofork f' g'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
e : c.pt ≅ c'.pt
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
comm₃ : e₁.inv ≫ c.π ≫ e.hom = c'.π
i : parallelPair f g ≅ parallelPair f' g' := parallelPair.ext e₀ e₁ ⋯ ⋯
⊢ π ((Cocone.precompose i.inv).obj c) ≫ e.hom = (e₁.inv ≫ c.π) ≫ e.hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ (fork f g).ι = ι f g

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ (fork f g).π.app zero = ι f g

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ Eq (α := equalizer f g ⟶ Y) (ι f g ≫ f) (ι f g ≫ g)

Tactic:
Fork.condition <| limit.cone <| parallelPair f g

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit, CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ Iso.hom (Iso.refl (limit.cone (parallelPair f g)).pt) ≫ (Fork.ofι (P := equalizer f g) (equalizer.ι f g) ⋯).ι =
    Fork.ι (limit.cone (parallelPair f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
k : W ⟶ X
h : k ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := equalizer f g) (lift k h) (ι f g) = k

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
k l : W ⟶ equalizer f g
h : k ≫ ι f g = l ≫ ι f g
⊢ k = l

Tactic:
Fork.IsLimit.hom_ext (limit.isLimit _) h

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
k : W ⟶ X
h : k ≫ f = k ≫ g
⊢ ∃! l : W ⟶ equalizer f g, l ≫ ι f g = k

Tactic:
Fork.IsLimit.existsUnique (limit.isLimit _) _ h

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.Fork.IsLimit.existsUnique, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
⊢ Mono c.ι

Tactic:
{ right_cancellation := fun _ _ w => Fork.IsLimit.hom_ext i w }

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext, CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Fork f g
m : s.pt ⟶ (idFork h_1).pt
h : m ≫ (idFork h_1).ι = s.ι
⊢ m ≫ (idFork h_1).ι = s.ι

Tactic:
h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Fork f g
m : s.pt ⟶ (idFork h_1).pt
h : m ≫ (idFork h_1).ι = s.ι
h₁ : (s.pt ⟶ (idFork h_1).pt) = (s.pt ⟶ X) → m = m ≫ (idFork h_1).ι
⊢ m = (fun (s : Fork f g) ↦ s.ι) s

Tactic:
convert! h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Fork f g
m : s.pt ⟶ (idFork h_1).pt
h : m ≫ (idFork h_1).ι = s.ι
e_1 : (s.pt ⟶ (idFork h_1).pt) = (s.pt ⟶ X)
⊢ m = m ≫ (idFork h_1).ι

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fork.ι, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Fork f g
m : s.pt ⟶ (idFork h_1).pt
h : m ≫ (idFork h_1).ι = s.ι
e_1 : (s.pt ⟶ (idFork h_1).pt) = (s.pt ⟶ X)
⊢ m = m ≫ (idFork h_1).ι

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h₀ : f = g
c : Fork f g
h : IsLimit c
⊢ IsIso c.ι

Tactic:
Iso.isIso_hom <| IsLimit.conePointUniqueUpToIso h <| isLimitIdFork h₀

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.isLimitIdFork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
h : f = g
⊢ IsIso (X := equalizer f g) (ι f g)

Tactic:
isIso_limit_cone_parallelPair_of_eq h <| limit.isLimit _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
c : Fork f f
h : IsLimit c
⊢ IsIso c.ι

Tactic:
isIso_limit_cone_parallelPair_of_eq rfl h

Premises used: CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
h : IsLimit c
inst_1 : Epi c.ι
⊢ IsIso c.ι

Tactic:
isIso_limit_cone_parallelPair_of_eq ((cancel_epi _).1 (Fork.condition c)) h

Premises used: CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, CategoryTheory.Limits.Fork.condition, Iff.mp, CategoryTheory.cancel_epi
-- 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
inst_1 : Epi t.ι
⊢ f = g

Tactic:
(cancel_epi (Fork.ι t)).1 <| Fork.condition t

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.Fork.ι, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : Epi (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
(cancel_epi (equalizer.ι f g)).1 <| equalizer.condition _ _

Premises used: CategoryTheory.Limits.equalizer.condition, CategoryTheory.Limits.equalizer.ι, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ HasEqualizer f f

Tactic:
HasLimit.mk
    { cone := idFork rfl
      isLimit := isLimitIdFork rfl }

Premises used: CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.isLimitIdFork, CategoryTheory.Limits.idFork, CategoryTheory.Limits.LimitCone.mk, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ IsIso (X := equalizer f f) (ι f f)

Tactic:
equalizer.ι_of_eq rfl

Premises used: CategoryTheory.Limits.equalizer.ι_of_eq, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).hom = ι f f

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
h : (isoSourceOfSelf f).inv ≫ ι f f = CategoryStruct.comp (Y := equalizer f f) (lift (𝟙 X) ⋯) (ι f f)
⊢ (isoSourceOfSelf f).inv = lift (𝟙 X) ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = CategoryStruct.comp (Y := equalizer f f) (lift (𝟙 X) ⋯) (ι f f)

Tactic:
simp [equalizer.isoSourceOfSelf]

Premises used: CategoryTheory.Limits.equalizer.isoSourceOfSelf
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
rw : c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g
rw₁ : c.fst ≫ s.ι ≫ f = c.fst ≫ s.ι ≫ g
rw₂ rw₃ : c.fst ≫ s.ι ≫ g = c.fst ≫ s.ι ≫ g
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g

Tactic:
rw [← c.condition_assoc, ← c.condition_assoc, s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition_assoc, CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
s' : Fork (h ≫ f) (h ≫ g)
⊢ (s'.ι ≫ h) ≫ f = (s'.ι ≫ h) ≫ g

Tactic:
simp [s'.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_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
⊢ ∀ (s_1 : Fork (h ≫ f) (h ≫ g)),
    (fun (s' : Fork (h ≫ f) (h ≫ g)) ↦ liftPrecomp h hs hc s') s_1 ≫ (precompFork h s c).ι = s_1.ι

Tactic:
simp [liftPrecomp, precompFork]

Premises used: CategoryTheory.Limits.liftPrecomp, CategoryTheory.Limits.precompFork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
h₀ : m ≫ c.fst = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.fst
h₁ : m ≫ c.snd = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.snd
⊢ ∀ (j : WalkingCospan), m ≫ c.π.app j = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.π.app j

Tactic:
apply PullbackCone.equalizer_ext

Premises used: CategoryTheory.Limits.PullbackCone.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
h₀ : m ≫ c.fst = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯)
⊢ m ≫ c.fst = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.fst

Tactic:
simp only [liftPrecomp, Fork.ofι_pt, IsLimit.fac, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.Fork.ofι_pt, CategoryTheory.Limits.liftPrecomp, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
h₀ : ∀ (j : WalkingParallelPair), (m ≫ c.fst) ≫ s.π.app j = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯) ≫ s.π.app j
⊢ m ≫ c.fst = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯)

Tactic:
apply hs.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
h₀ : (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯) ≫ s.ι
⊢ ∀ (j : WalkingParallelPair), (m ≫ c.fst) ≫ s.π.app j = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯) ≫ s.π.app j

Tactic:
apply Fork.equalizer_ext

Premises used: CategoryTheory.Limits.Fork.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ c.snd = s'.ι
⊢ (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯) ≫ s.ι

Tactic:
simp [c.condition, reassoc_of% h]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
⊢ m ≫ c.snd = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.snd

Tactic:
simpa [liftPrecomp] using h

Premises used: CategoryTheory.Limits.liftPrecomp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
⊢ HasEqualizer (h ≫ f) (h ≫ g)

Tactic:
HasLimit.mk
    { cone := precompFork h s c
      isLimit := isLimitPrecompFork h hs hc }

Premises used: CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.precompFork, CategoryTheory.Limits.isLimitPrecompFork, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
inst_1 : HasEqualizer f g
inst_2 : HasPullback (X := equalizer f g) (equalizer.ι f g) h
⊢ HasEqualizer (h ≫ f) (h ≫ g)

Tactic:
hasEqualizer_precomp_of_equalizer h
    (equalizerIsEqualizer f g) (pullback.isLimit (equalizer.ι f g) h)

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.equalizer.ι, CategoryTheory.Limits.hasEqualizer_precomp_of_equalizer, CategoryTheory.Limits.equalizerIsEqualizer
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
⊢ (cofork f g).π = π f g

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
⊢ (cofork f g).ι.app one = π f g

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
⊢ Eq (α := X ⟶ coequalizer f g) (f ≫ π f g) (g ≫ π f g)

Tactic:
Cofork.condition <| colimit.cocone <| parallelPair f g

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
⊢ Cofork.π (colimit.cocone (parallelPair f g)) ≫ Iso.hom (Iso.refl (colimit.cocone (parallelPair f g)).pt) =
    (Cofork.ofπ (P := coequalizer f g) (coequalizer.π f g) ⋯).π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
W : C
k : Y ⟶ W
h : f ≫ k = g ≫ k
⊢ CategoryStruct.comp (Y := coequalizer f g) (π f g) (desc k h) = k

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst_2 : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
rw :
  (parallelPairHom f g f' g' p q wf wg).app one ≫
      CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) =
    q ≫ h
rw₁ :
  q ≫ CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) = q ≫ h
rw₂ rw₃ : q ≫ h = q ≫ h
⊢ CategoryStruct.comp (Y := coequalizer f g) (π f g)
      (CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimMap (parallelPairHom f g f' g' p q wf wg))
        (desc h wh)) =
    q ≫ h

Tactic:
rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]

Premises used: CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.parallelPairHom_app_one, CategoryTheory.Limits.coequalizer.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
W : C
k l : coequalizer f g ⟶ W
h : π f g ≫ k = π f g ≫ l
⊢ k = l

Tactic:
Cofork.IsColimit.hom_ext (colimit.isColimit _) h

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
W : C
k : Y ⟶ W
h : f ≫ k = g ≫ k
⊢ ∃! d : coequalizer f g ⟶ W, π f g ≫ d = k

Tactic:
Cofork.IsColimit.existsUnique (colimit.isColimit _) _ h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cofork.IsColimit.existsUnique, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
⊢ Epi c.π

Tactic:
{ left_cancellation := fun _ _ w => Cofork.IsColimit.hom_ext i w }

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Epi.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Cofork f g
m : (idCofork h_1).pt ⟶ s.pt
h : (idCofork h_1).π ≫ m = s.π
⊢ (idCofork h_1).π ≫ m = s.π

Tactic:
h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Cofork f g
m : (idCofork h_1).pt ⟶ s.pt
h : (idCofork h_1).π ≫ m = s.π
h₁ : ((idCofork h_1).pt ⟶ s.pt) = (Y ⟶ s.pt) → m = (idCofork h_1).π ≫ m
⊢ m = (fun (s : Cofork f g) ↦ s.π) s

Tactic:
convert! h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Cofork f g
m : (idCofork h_1).pt ⟶ s.pt
h : (idCofork h_1).π ≫ m = s.π
e_1 : ((idCofork h_1).pt ⟶ s.pt) = (Y ⟶ s.pt)
⊢ m = (idCofork h_1).π ≫ m

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp, 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
h_1 : f = g
s : Cofork f g
m : (idCofork h_1).pt ⟶ s.pt
h : (idCofork h_1).π ≫ m = s.π
e_1 : ((idCofork h_1).pt ⟶ s.pt) = (Y ⟶ s.pt)
⊢ m = (idCofork h_1).π ≫ m

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h₀ : f = g
c : Cofork f g
h : IsColimit c
⊢ IsIso c.π

Tactic:
Iso.isIso_hom <| IsColimit.coconePointUniqueUpToIso (isColimitIdCofork h₀) h

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.isColimitIdCofork, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
h : f = g
⊢ IsIso (Y := coequalizer f g) (π f g)

Tactic:
isIso_colimit_cocone_parallelPair_of_eq h <| colimit.isColimit _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
c : Cofork f f
h : IsColimit c
⊢ IsIso c.π

Tactic:
isIso_colimit_cocone_parallelPair_of_eq rfl h

Premises used: CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
h : IsColimit c
inst_1 : Mono c.π
⊢ IsIso c.π

Tactic:
isIso_colimit_cocone_parallelPair_of_eq ((cancel_mono _).1 (Cofork.condition c)) h

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.Limits.Cofork.condition, Iff.mp