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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
⊢ ∀ {X Y : CostructuredArrow (S.prod S') (T, T')} (f : X ⟶ Y),
    (𝟭 (CostructuredArrow (S.prod S') (T, T'))).map f ≫
        (Iso.refl ((𝟭 (CostructuredArrow (S.prod S') (T, T'))).obj Y)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (S.prod S') (T, T'))).obj X)).hom ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f

Tactic:
by 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✝ Y✝ : CostructuredArrow L (R.obj b)
f : X✝ ⟶ Y✝
⊢ L.map f.left ≫
      (CostructuredArrow.left
          { left := { left := Y✝.left, right := b, hom := Y✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b }).hom =
    (CostructuredArrow.left
          { left := { left := X✝.left, right := b, hom := X✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b }).hom ≫
      R.map (𝟙 b)

Tactic:
by 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✝ 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:
by 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:
by 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:
by 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:
by 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✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ (v ≫ q) ≫ h = 𝟙 (image f) ≫ h

Tactic:
t

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ h = 𝟙 (image f) ≫ h
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (preComp f g)

Tactic:
by
  apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)
  exact epi_comp _ _

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
⊢ factorThruImage f.hom ≫ map sq = Arrow.Hom.left sq ≫ factorThruImage g.hom

Tactic:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
t : Fork f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝, π := π✝ } ⟶ t
⊢ f.hom ≫ t.ι = ι { pt := pt✝, π := π✝ }

Tactic:
cases t

Goal state after:
case mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y) ≫
      h =
    y

Tactic:
by
            apply image.ext
            simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc]

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

Goal state before:
pp: case mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
t : Cofork f✝ g
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝, ι := ι✝ } ⟶ t
⊢ Cofork.π { pt := pt✝, ι := ι✝ } ≫ f.hom = t.π

Tactic:
cases t

Goal state after:
case mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.hom = Cofork.π { pt := pt✝, ι := ι✝ }
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:
by 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:
by 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✝ : Mono 0
⊢ (0 ≫ 0) ≫ 0 = 𝟙 X ≫ 0

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
⊢ G.map (f ≫ coequalizer.π f g) = G.map (g ≫ coequalizer.π f g)

Tactic:
rw [coequalizer.condition]

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:
by 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:
by 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✝ : IsSplitEpi f
⊢ 𝟙 X ≫ f = (f ≫ section_ f) ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((colimit.isColimit F).desc c)

Tactic:
change IsIso ((Cocone.forget _).map ((colimit.isColimit F).descCoconeMorphism c))

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((Cocone.forget F).map ((colimit.isColimit F).descCoconeMorphism c))
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), f ≫ (x + y) = f ≫ x + f ≫ y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (m : R) (x : Y ⟶ Z), f ≫ (m • x) = (RingHom.id R) m • f ≫ x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (x + y) ≫ g = x ≫ g + y ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (m : R) (x : X ⟶ Y), (m • x) ≫ g = (RingHom.id R) m • x ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ ∀ {X Y : C} (x : X ≅ Y), ⊤ X → ⊤ Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
⊢ (⨆ a, P a) X ↔ ∃ a, P a X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.Nonempty ↔ ¬P = ⊥

Tactic:
by
  rw [ne_bot_iff_exists, nonempty_iff]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
by
    have := preservesSmallestLimits_of_preservesLimits F
    exact preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
hY : P Y
e : X ≅ Y
⊢ ⊤ { obj := Y, property := hY }

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
⊢ hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c ≫ e.hom = s

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf' : IsLimit kf'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ (Fork.ι kf ≫ Arrow.Hom.left φ) ≫ f' = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf.mapOfIsLimit hf' φ.hom ≫ kf'.mapOfIsLimit hf φ.inv) ≫ Fork.ι kf = 𝟙 kf.pt ≫ Fork.ι kf

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf'.mapOfIsLimit hf φ.inv ≫ kf.mapOfIsLimit hf' φ.hom) ≫ Fork.ι kf' = 𝟙 kf'.pt ≫ Fork.ι kf'

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : Epi (kernel.ι f)
⊢ kernel.ι f ≫ f = kernel.ι f ≫ 0

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel f
inst✝ : Mono g
⊢ kernel.ι f ≫ f ≫ g = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
⊢ (kernel.ι g ≫ inv f) ≫ f ≫ g = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
⊢ (Fork.ι s ≫ f) ≫ g = 0

Tactic:
by simp

Goal state after: