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
inst_1 : Mono t.π
⊢ f = g

Tactic:
(cancel_mono (Cofork.π t)).1 <| Cofork.condition t

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.Cofork.condition, Iff.mp, 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
inst_1 : HasCoequalizer f g
inst_2 : Mono (Y := coequalizer f g) (coequalizer.π f g)
⊢ f = g

Tactic:
(cancel_mono (coequalizer.π f g)).1 <| coequalizer.condition _ _

Premises used: CategoryTheory.Limits.coequalizer.condition, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Limits.coequalizer.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ HasCoequalizer f f

Tactic:
HasColimit.mk
    { cocone := idCofork rfl
      isColimit := isColimitIdCofork rfl }

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.idCofork, CategoryTheory.Limits.isColimitIdCofork, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ IsIso (Y := coequalizer f f) (π f f)

Tactic:
coequalizer.π_of_eq rfl

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

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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ π f f ≫ (isoTargetOfSelf f).hom = CategoryStruct.comp (Y := coequalizer f f) (π f f) (desc (𝟙 Y) ⋯)

Tactic:
simp [coequalizer.isoTargetOfSelf]

Premises used: CategoryTheory.Limits.coequalizer.isoTargetOfSelf
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoTargetOfSelf f).inv = π f f

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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
simp : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g) ≫ G.map f) (G.map (equalizer.ι f g) ≫ G.map g)

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
rw rw₁ : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ g)) (G.map (equalizer.ι f g ≫ g))
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))

Tactic:
rw [equalizer.condition]

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj X)
    (CategoryStruct.comp (Y := equalizer (G.map f) (G.map g)) (equalizerComparison f g G)
      (equalizer.ι (G.map f) (G.map g)))
    (G.map (equalizer.ι f g))

Tactic:
equalizer.lift_ι _ _

Premises used: CategoryTheory.Limits.equalizer.lift_ι, CategoryTheory.Limits.equalizerComparison, 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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
h₁ :
  CategoryStruct.comp (Y := equalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (equalizer f g)) (G.map (equalizer.lift h w)) (equalizerComparison f g G))
      (equalizer.ι (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := equalizer (G.map f) (G.map g)) (equalizer.lift (G.map h) ⋯)
      (equalizer.ι (G.map f) (G.map g))
⊢ Eq (α := G.obj Z ⟶ equalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (equalizer f g)) (G.map (equalizer.lift h w)) (equalizerComparison f g G))
    (equalizer.lift (G.map h) ⋯)

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ CategoryStruct.comp (Y := equalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (equalizer f g)) (G.map (equalizer.lift h w)) (equalizerComparison f g G))
      (equalizer.ι (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := equalizer (G.map f) (G.map g)) (equalizer.lift (G.map h) ⋯)
      (equalizer.ι (G.map f) (G.map g))

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
simp : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map f ≫ G.map (coequalizer.π f g))
    (G.map g ≫ G.map (coequalizer.π f g))

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
rw rw₁ : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (g ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))

Tactic:
rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
⊢ Eq (α := G.obj Y ⟶ G.obj (coequalizer f g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizerComparison f g G))
    (G.map (coequalizer.π f g))

Tactic:
coequalizer.π_desc _ _

Premises used: CategoryTheory.Limits.coequalizerComparison, CategoryTheory.Limits.colimit.desc, 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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
h₁ :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (G.map (coequalizer.desc h w))) =
    CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizer.desc (G.map h) ⋯)
⊢ Eq (α := coequalizer (G.map f) (G.map g) ⟶ G.obj Z)
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G) (G.map (coequalizer.desc h w)))
    (coequalizer.desc (G.map h) ⋯)

Tactic:
apply coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (G.map (coequalizer.desc h w))) =
    CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizer.desc (G.map h) ⋯)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)
⊢ HasEqualizers.{v, u} C

Tactic:
{ has_limit := fun F => hasLimit_of_iso (diagramIsoParallelPair F).symm }

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)
⊢ HasCoequalizers.{v, u} C

Tactic:
{ has_colimit := fun F => hasColimit_of_iso (diagramIsoParallelPair F) }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoParallelPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsSplitMono f
⊢ f ≫ 𝟙 Y = f ≫ retraction f ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitMono f
⊢ Fork.ι (coneOfIsSplitMono f) = f

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
dsimp : (s.ι ≫ retraction f) ≫ f = s.ι
⊢ (s.ι ≫ retraction f) ≫ Fork.ι (coneOfIsSplitMono f) = s.ι

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
rw : s.ι ≫ 𝟙 Y = s.ι
⊢ (s.ι ≫ retraction f) ≫ f = s.ι

Tactic:
rw [Category.assoc, ← s.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_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ s.ι ≫ 𝟙 Y = s.ι

Tactic:
apply Category.comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
m : s.pt ⟶ Cone.pt (F := parallelPair (𝟙 Y) (retraction f ≫ f)) (coneOfIsSplitMono f)
hm : m ≫ Fork.ι (coneOfIsSplitMono f) = s.ι
⊢ m = s.ι ≫ retraction f

Tactic:
simp [← hm]
-- 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
Z : C
h : Y ⟶ Z
hm : Mono h
simp : (c.ι ≫ f) ≫ h = (c.ι ≫ g) ≫ h
⊢ c.ι ≫ f ≫ h = c.ι ≫ g ≫ h

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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
⊢ (c.ι ≫ f) ≫ h = (c.ι ≫ g) ≫ h

Tactic:
congrArg (· ≫ h) c.condition

Premises used: congrArg, CategoryTheory.Limits.Fork.condition, 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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
⊢ (c.ι ≫ f) ≫ h = (c.ι ≫ g) ≫ h

Tactic:
exact congrArg (· ≫ h) c.condition

Premises used: congrArg, CategoryTheory.Limits.Fork.condition, 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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
this : c.ι ≫ f ≫ h = c.ι ≫ g ≫ h
⊢ c.ι ≫ f ≫ h = c.ι ≫ g ≫ h

Tactic:
simp [this]
-- 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
Z : C
h : Y ⟶ Z
hm : Mono h
s : Fork (f ≫ h) (g ≫ h)
a : (s.ι ≫ f) ≫ h = (s.ι ≫ g) ≫ h
⊢ s.ι ≫ f = s.ι ≫ g

Tactic:
apply hm.right_cancellation

Premises used: CategoryTheory.Mono.right_cancellation
-- 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
Z : C
h : Y ⟶ Z
hm : Mono h
s : Fork (f ≫ h) (g ≫ h)
⊢ (s.ι ≫ f) ≫ h = (s.ι ≫ g) ≫ h

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 g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ (Fork.ofι c.ι ⋯).ι = s.ι
apply : m ≫ c.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
⊢ m = (↑l : s'.pt ⟶ c.pt)

Tactic:
apply Fork.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- 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
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m ≫ c.ι = s.ι

Tactic:
rw [Fork.ι_ofι] at hm

Premises used: CategoryTheory.Limits.Fork.ι_ofι
-- 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
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ c.ι = s.ι
rw : s.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
⊢ m ≫ c.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι

Tactic:
rw [hm]
-- 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
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ c.ι = s.ι
⊢ s.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι

Tactic:
l.2.symm

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.ι, Eq.symm, CategoryTheory.Limits.parallelPair, Subtype.property
-- 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
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ c.ι = s.ι
⊢ s.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι

Tactic:
exact l.2.symm

Premises used: Eq.symm, Subtype.property
-- 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
Z : C
h : Y ⟶ Z
inst_2 : Mono h
⊢ HasEqualizer (f ≫ h) (g ≫ h)

Tactic:
⟨⟨{   cone := _
        isLimit := isEqualizerCompMono (limit.isLimit _) h }⟩⟩

Premises used: CategoryTheory.Limits.isEqualizerCompMono._proof_2, CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.limit.cone, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.isEqualizerCompMono._proof_1, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.isEqualizerCompMono, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
⊢ f ≫ 𝟙 X = f ≫ f

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := ⋯
rw : c.ι ≫ 𝟙 X = c.ι
⊢ c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 c.pt

Tactic:
rw [← cancel_mono_id c.ι, Category.assoc, Fork.IsLimit.lift_ι, Fork.ι_ofι, ← c.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.Fork.ι, CategoryTheory.cancel_mono_id, CategoryTheory.Limits.Fork.ι_ofι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := ⋯
⊢ c.ι ≫ 𝟙 X = c.ι

Tactic:
Category.comp_id c.ι

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := ⋯
⊢ c.ι ≫ 𝟙 X = c.ι

Tactic:
exact Category.comp_id c.ι

Premises used: CategoryTheory.Category.comp_id, 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
inst_1 : IsSplitEpi f
⊢ 𝟙 X ≫ f = (f ≫ section_ f) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitEpi f
⊢ Cofork.π (coconeOfIsSplitEpi f) = f

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
dsimp : f ≫ section_ f ≫ s.π = s.π
⊢ Cofork.π (coconeOfIsSplitEpi f) ≫ section_ f ≫ s.π = s.π

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
rw : (f ≫ section_ f) ≫ s.π = s.π
rw₁ : 𝟙 X ≫ s.π = s.π
rw₂ rw₃ : s.π = s.π
⊢ f ≫ section_ f ≫ s.π = s.π

Tactic:
rw [← Category.assoc, ← s.condition, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
m : Cocone.pt (F := parallelPair (𝟙 X) (f ≫ section_ f)) (coconeOfIsSplitEpi f) ⟶ s.pt
hm : Cofork.π (coconeOfIsSplitEpi f) ≫ m = s.π
⊢ m = section_ f ≫ s.π

Tactic:
simp [← hm]
-- 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
W : C
h : W ⟶ X
hm : Epi h
simp : h ≫ f ≫ c.π = h ≫ g ≫ c.π
⊢ (h ≫ f) ≫ c.π = (h ≫ g) ≫ c.π

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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
⊢ h ≫ f ≫ c.π = h ≫ g ≫ c.π

Tactic:
congrArg (h ≫ ·) c.condition

Premises used: congrArg, CategoryTheory.Limits.Cofork.condition, 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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
⊢ h ≫ f ≫ c.π = h ≫ g ≫ c.π

Tactic:
exact congrArg (h ≫ ·) c.condition

Premises used: congrArg, CategoryTheory.Limits.Cofork.condition, 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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
a : h ≫ f ≫ s.π = h ≫ g ≫ s.π
⊢ f ≫ s.π = g ≫ s.π

Tactic:
apply hm.left_cancellation

Premises used: CategoryTheory.Epi.left_cancellation
-- 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
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
a : (h ≫ f) ≫ s.π = (h ≫ g) ≫ s.π
⊢ h ≫ f ≫ s.π = h ≫ g ≫ s.π

Tactic:
simp_rw [← Category.assoc, s.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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm_1 : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m = s.π
apply : c.π ≫ m = c.π ≫ (↑l : c.pt ⟶ s'.pt)
⊢ m = (↑l : c.pt ⟶ s'.pt)

Tactic:
apply Cofork.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- 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
W : C
h : W ⟶ X
hm_1 : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m = s.π
⊢ c.π ≫ m = s.π

Tactic:
rw [Cofork.π_ofπ] at hm

Premises used: CategoryTheory.Limits.Cofork.π_ofπ