mathlib-initiative/mathlib-tactics huggingface dataset:
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)), kernel.lift g (Fork.ι s ≫ f) ⋯ ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s

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
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biprodComparison' X Y ≫ F.biprodComparison X Y = 𝟙 (F.obj X ⊞ F.obj Y)

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.ι (f ≫ g) ≫ 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
X' Y' : C
f' : X' ⟶ Y'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
⊢ (parallelPair f 0).map WalkingParallelPairHom.right ≫ eY.hom =
    eX.hom ≫ (parallelPair f' 0).map WalkingParallelPairHom.right

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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s✝ : KernelFork f
hs : IsLimit s✝
s : Fork l 0
⊢ hs.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι (KernelFork.ofι (Fork.ι s✝) ⋯) = 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
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
⊢ (e.hom ≫ Cofork.π c) ≫ hc.desc (ofπ (e.inv ≫ s) ⋯) = 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'
cc : CokernelCofork f
cc' : CokernelCofork f'
hf : IsColimit cc
hf' : IsColimit cc'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ Cofork.π cc ≫ mapOfIsColimit hf cc' φ.hom ≫ mapOfIsColimit hf' cc φ.inv = Cofork.π cc ≫ 𝟙 cc.pt

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'
cc : CokernelCofork f
cc' : CokernelCofork f'
hf : IsColimit cc
hf' : IsColimit cc'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ Cofork.π cc' ≫ mapOfIsColimit hf' cc φ.inv ≫ mapOfIsColimit hf cc' φ.hom = Cofork.π cc' ≫ 𝟙 cc'.pt

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✝¹ : HasCokernel f
inst✝ : Mono (cokernel.π f)
⊢ f ≫ cokernel.π f = 0 ≫ cokernel.π 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✝ : HasCokernel f
⊢ 0 ≫ 𝟙 Y = 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✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
⊢ (f ≫ g) ≫ inv g ≫ cokernel.π 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✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
⊢ ∀ (s : CokernelCofork (f ≫ g)),
    Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ cokernel.desc f (g ≫ Cofork.π s) ⋯ = Cofork.π 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✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Epi f
inst✝ : HasCokernel g
⊢ (f ≫ g) ≫ cokernel.π 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✝ f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasImage f
inst✝ : HasKernel (factorThruImage f)
⊢ factorThruImage f ≫ image.ι f = f

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F f : J → C
t : Cone (Discrete.functor f)
ht : IsLimit t
j j' : J
⊢ ht.lift (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.π.app { as := j' } =
    if h : j = j' then eqToHom ⋯ else 0

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F f : J → C
t : Cocone (Discrete.functor f)
ht : IsColimit t
j j' : J
⊢ t.ι.app { as := j } ≫ ht.desc (Cofan.mk (f j') fun j'_1 ↦ if h : j'_1 = j' then eqToHom ⋯ else 0) =
    if h : j = j' then eqToHom ⋯ else 0

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
⊢ ∀ (j : Discrete K),
    (c.whisker g).toCone.π.app j =
      (Iso.refl (c.whisker g).toCone.pt).hom ≫
        ((Cone.postcompose (Discrete.functorComp f ⇑g).inv).obj
                (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone)).π.app
          j

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
⊢ ∀ (j : Discrete K),
    (c.whisker g).toCocone.ι.app j ≫ (Iso.refl (c.whisker g).toCocone.pt).hom =
      ((Cocone.precompose (Discrete.functorComp f ⇑g).hom).obj
              (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone)).ι.app
        j

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
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
s✝ : CokernelCofork f
hs : IsColimit s✝
s : Cofork l 0
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π s✝) ⋯) ≫ hs.desc (CokernelCofork.ofπ s.π ⋯) = s.π

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ ι f j ≫ π f j = 𝟙 (f j)

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'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
⊢ (parallelPair f 0).map WalkingParallelPairHom.right ≫ eY.hom =
    eX.hom ≫ (parallelPair f' 0).map WalkingParallelPairHom.right

Tactic:
by simp

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
⊢ g k = g (e (e.symm k))

Tactic:
by simp

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
⊢ g (e (e.symm k)) = g k

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
inst✝ : HasKernels C
f g : Arrow C
u : f ⟶ g
⊢ (kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
e : C ≌ D
inst✝ : e.functor.Additive
f g : D
f✝ g✝ : f ⟶ g
⊢ e.functor.map (e.inverse.map (f✝ + g✝)) = e.functor.map (e.inverse.map f✝ + e.inverse.map g✝)

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ ∀ (j : J), fromSubtype f p ≫ π f j = (lift fun j ↦ if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π f j

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ ∀ (j : J), ι f j ≫ toSubtype f p = ι f j ≫ desc fun j ↦ if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Cone (Discrete.functor f)
ht : IsLimit t
⊢ ∀ (j : Discrete J), t.π.app j = (Iso.refl t.pt).hom ≫ (Bicone.ofLimitCone ht).toCone.π.app j

Tactic:
by simp

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
⊢ (fromSubtype f fun j ↦ j ≠ i) ≫ π f i = 0

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.ι WalkingPair.left ≫ b.π WalkingPair.left = 𝟙 X

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.ι WalkingPair.left ≫ b.π WalkingPair.right = 0

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.ι WalkingPair.right ≫ b.π WalkingPair.left = 0

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.ι WalkingPair.right ≫ b.π WalkingPair.right = 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
⊢ (ι f i ≫ toSubtype f fun j ↦ j ≠ i) = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cone (pair X Y)
ht : IsLimit t
⊢ ((BinaryBicone.ofLimitCone ht).fst ≫ (BinaryBicone.ofLimitCone ht).inl +
        (BinaryBicone.ofLimitCone ht).snd ≫ (BinaryBicone.ofLimitCone ht).inr) ≫
      BinaryFan.fst t =
    𝟙 (BinaryBicone.ofLimitCone ht).pt ≫ BinaryFan.fst t

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cone (pair X Y)
ht : IsLimit t
⊢ ((BinaryBicone.ofLimitCone ht).fst ≫ (BinaryBicone.ofLimitCone ht).inl +
        (BinaryBicone.ofLimitCone ht).snd ≫ (BinaryBicone.ofLimitCone ht).inr) ≫
      BinaryFan.snd t =
    𝟙 (BinaryBicone.ofLimitCone ht).pt ≫ BinaryFan.snd t

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (𝟙 Y - (𝟙 Y - retraction f ≫ f)) ≫ Cofork.π c = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
⊢ 𝟙 Y - (𝟙 Y - retraction f ≫ f) = retraction f ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
i' : IsColimit c' := isCokernelEpiComp i (retraction f) ⋯
i'' : IsColimit (coforkOfCokernelCofork c') := isColimitCoforkOfCokernelCofork i'
⊢ (𝟙 Y - retraction f ≫ f) ≫ (𝟙 Y - retraction f ≫ f) = 𝟙 Y - retraction f ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ retraction f = 𝟙 X

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ Cofork.π c = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.fst b.toCone = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.snd b.toCone = g

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N O : ModuleCat 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.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.fst b.toCone = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.snd b.toCone = g

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x : ↑(AddCommGrpCat.of ↑M)
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom { toFun := fun m ↦ 1 • m, map_zero' := ⋯, map_add' := ⋯ })) x =
    (ConcreteCategory.hom 1) x

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x : ↑(AddCommGrpCat.of ↑M)
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom { toFun := fun m ↦ 0 • m, map_zero' := ⋯, map_add' := ⋯ })) x =
    (ConcreteCategory.hom 0) x

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inl b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inr b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = g

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : AlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
i : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
i : X ≅ Y
x : ↑Y
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by simp

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ (braiding P Q).hom ≫ (braiding Q P).hom = 𝟙 (P ⊞ Q)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
⊢ ∀ (x y : R) (b : ↑(mkOfSMul' φ)), (x * y) • b = x • y • b

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
⊢ ∀ (b : ↑(mkOfSMul' φ)), 1 • b = b

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
⊢ ∀ (x : ↑(mkOfSMul' φ)), 0 • x = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
A : AlgCat ℤ
x✝ : ℤ
⊢ (RingEquiv.refl ↑A) ((algebraMap ℤ ↑A) x✝) = (algebraMap ℤ ↑((forget₂ (AlgCat ℤ) RingCat).obj A)) x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
G : ModuleCat R
H : Type u
inst✝¹ : AddCommGroup 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.Basic

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inl b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso (biprod.map g f)

Tactic:
rw [← biprod.braiding_map_braiding]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso ((biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inr b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = g

Tactic:
by simp

Goal state after: