mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow L (R.obj b)
f : X✝ ⟶ Y✝
⊢ (snd L R).map { left := f.left, right := 𝟙 b, w := ⋯ } ≫
      CostructuredArrow.hom
        { left := { left := Y✝.left, right := b, hom := Y✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b } =
    CostructuredArrow.hom
      { left := { left := X✝.left, right := b, hom := X✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X : CostructuredArrow (snd L R) b
⊢ L.map (𝟙 X.left.left) ≫ ((costructuredArrowSndProj L R b ⋙ costructuredArrowSndInclusion L R b).obj X).left.hom =
    ((𝟭 (CostructuredArrow (snd L R) b)).obj X).left.hom ≫ R.map X.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X : CostructuredArrow (snd L R) b
⊢ (snd L R).map { left := 𝟙 X.left.left, right := X.hom, w := ⋯ } ≫
      ((costructuredArrowSndProj L R b ⋙ costructuredArrowSndInclusion L R b).obj X).hom =
    ((𝟭 (CostructuredArrow (snd L R) b)).obj X).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X : CostructuredArrow L (R.obj b)
⊢ L.map (𝟙 X.left) ≫ ((𝟭 (CostructuredArrow L (R.obj b))).obj X).hom =
    ((costructuredArrowSndInclusion L R b ⋙ costructuredArrowSndProj L R b).obj X).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N O : SemimoduleCat R
f : M ⟶ N
g : N ⟶ O
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
e : M ≅ N
x : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} 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

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
G : SemimoduleCat R
H : Type u
inst✝¹ : AddCommMonoid H
inst✝ : Module R H
f : ↑G →ₗ[R] H
⊢ f ∘ₗ Hom.hom (𝟙 G) = f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
G : Type u
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
H : SemimoduleCat R
f : G →ₗ[R] ↑H
⊢ Hom.hom (𝟙 H) ∘ₗ f = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f g : X✝ ⟶ Y
F : 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : HasImage f.hom
⊢ 𝟙 (image f.hom) ≫ image.ι f.hom = image.ι f.hom ≫ Arrow.Hom.right (𝟙 f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f g : X✝ ⟶ Y
F : 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ (factorThruImage f.hom ≫ m.map) ≫ image.ι g.hom = (Arrow.Hom.left sq ≫ factorThruImage g.hom) ≫ image.ι g.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f g : X✝ ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
X : WalkingParallelPair
⊢ F.obj X = (parallelPair (F.map left) (F.map right)).obj X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f g : X✝ ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj X = F.obj X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X✝ : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
⊢ ∀ (s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫
        ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j =
      s.π.app j

Tactic:
intro s j

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
j : J
⊢ h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫
      ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j =
    s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ factorThruImage f.hom ≫ map sq = Arrow.Hom.left sq ≫ factorThruImage g.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ map sq ≫ ι g.hom = ι f.hom ≫ Arrow.Hom.right sq

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ 𝟙 X ≫ 0 = 0 ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ 0 ≫ 𝟙 Y = 0 ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : StrongEpi f
⊢ f ≫ 𝟙 Y = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasImages C
inst✝ : HasStrongEpiImages C
f g : Arrow C
st : f ⟶ g
⊢ (Arrow.Hom.left st ≫ factorThruImage g.hom) ≫ image.ι g.hom =
    factorThruImage f.hom ≫ image.ι f.hom ≫ Arrow.Hom.right st

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝¹ : Category.{v, u} C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (Iso.refl (limit.cone (parallelPair f g)).pt).hom ≫ (Fork.ofι (equalizer.ι f g) ⋯).ι =
    Fork.ι (limit.cone (parallelPair f g))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
⊢ ∀ (s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)) (j : J),
    ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫
        h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } =
      s.ι.app j

Tactic:
intro s j

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
j : J
⊢ ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫
      h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } =
    s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
x✝ : Mono 0
⊢ (0 ≫ 0) ≫ 0 = 𝟙 X ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
x✝ : Epi 0
⊢ 0 ≫ 0 ≫ 0 = 0 ≫ 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝¹ : Category.{v, u} C
f g : X ⟶ Y
inst✝ : HasCoequalizer f g
⊢ Cofork.π (colimit.cocone (parallelPair f g)) ≫ (Iso.refl (colimit.cocone (parallelPair f g)).pt).hom =
    (Cofork.ofπ (coequalizer.π f g) ⋯).π

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝¹ : Category.{v, u} C
f g : X ⟶ Y
inst✝ : IsSplitMono f
⊢ f ≫ 𝟙 Y = f ≫ retraction f ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ ι f = 0

Tactic:
image.eq_fac h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 ≫ F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
X✝ Y✝ : D
f : X✝ ⟶ Y✝
x✝ : D
⊢ F.map (f ≫ hF.preimage 0) = F.map (hF.preimage 0)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
x✝² x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
⊢ F.map (hF.preimage 0 ≫ f) = F.map (hF.preimage 0)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
inst✝² : HasZeroMorphisms E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : G.PreservesZeroMorphisms
⊢ ∀ (X Y : C), (F ⋙ G).map 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := mono_of_isLimit_fork i
⊢ c.ι ≫ (Fork.ofι f ⋯).ι = c.ι

Tactic:
Fork.ι_ofι,

Goal state after:
C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := mono_of_isLimit_fork i
⊢ c.ι ≫ f = c.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝¹ : Category.{v, u} C
f g : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 X ≫ f = (f ≫ section_ f) ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
⊢ ∀ (s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫
        { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j =
      s.π.app j

Tactic:
intro s j

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
j : J
⊢ h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫
      { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j =
    s.π.app j