mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel h
inst✝ : HasKernel f
w₂ : f = h
⊢ kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

Tactic:
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:
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 ≫ g) ≫ f) ≫ g = 0 ≫ g

Tactic:
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:
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:
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:
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)), kernel.lift g (Fork.ι s ≫ f) ⋯ ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s

Tactic:
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:
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)
m : s.pt ⟶ kernel g
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m ≫ equalizer.ι g 0 = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯ ≫ equalizer.ι g 0

Tactic:
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:
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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
⊢ 0 ≫ f = 0

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

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

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
as✝ : J
⊢ G.map (g { as := as✝ }.as) ≫ 𝟙 (G.obj (f { as := as✝ }.as)) = 𝟙 (G.obj P) ≫ G.map (g { as := as✝ }.as)

Tactic:
simp

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

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
as✝ : J
⊢ (𝟙 (G.obj (f { as := as✝ }.as)) ≫ G.map (g { as := as✝ }.as)) ≫ 𝟙 (G.obj P) = G.map (g { as := as✝ }.as)

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.inv ≫ (i.hom ≫ Fork.ι s) ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct fun j ↦ G.obj (f j)
inst✝ : IsIso (sigmaComparison G f)
j : J
⊢ G.map (Sigma.ι f j) ≫ inv (sigmaComparison G f) = Sigma.ι (fun x ↦ G.obj (f x)) j

Tactic:
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
s : CokernelCofork f
⊢ s.ι.app zero = 0

Tactic:
simp

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

Tactic:
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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
⊢ (g ≫ f) ≫ Cofork.π c = 0

Tactic:
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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ 0 ≫ s.π = g ≫ 0 ≫ s.π

Tactic:
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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s

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

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) ≫ cokernel.desc f g h = 0

Tactic:
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
W : C
h : f ≫ 0 = 0
⊢ coequalizer.π f 0 ≫ desc f 0 h = coequalizer.π f 0 ≫ 0

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

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

Goal state before:
pp: case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).hom = cokernel.π f

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).inv = cokernel.π f

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
inst✝ : HasCokernel f
he : f ≫ e = 0
⊢ (cokernelIsoOfEq ⋯).hom ≫ cokernel.desc f e he = cokernel.desc f e ⋯

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
he : f ≫ e = 0
inst✝ : HasCokernel f
⊢ (cokernelIsoOfEq ⋯).inv ≫ cokernel.desc f e he = cokernel.desc f e ⋯

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel h
inst✝ : HasCokernel f
w₂ : f = h
⊢ cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯

Tactic:
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:
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:
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)
m : cokernel f ⟶ s.pt
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ coequalizer.π f 0 ≫ m =
    coequalizer.π f 0 ≫ cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯

Tactic:
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:
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.π (f ≫ g) = f ≫ 0

Tactic:
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:
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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
⊢ f ≫ 0 = 0

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

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

Goal state before:
pp: case refine_1
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
hc : (c.whisker g).IsBilimit
⊢ IsLimit c.toCone

pp: case refine_2
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
hc : (c.whisker g).IsBilimit
⊢ IsColimit c.toCocone

pp: case refine_3
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
hc : c.IsBilimit
⊢ IsLimit (c.whisker g).toCone

pp: case refine_4
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
hc : c.IsBilimit
⊢ IsColimit (c.whisker g).toCocone

Tactic:
· let := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
    let := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
    exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this

Goal state after:
case refine_2
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
hc : (c.whisker g).IsBilimit
⊢ IsColimit c.toCocone

case refine_3
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
hc : c.IsBilimit
⊢ IsLimit (c.whisker g).toCone

case refine_4
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
hc : c.IsBilimit
⊢ IsColimit (c.whisker g).toCocone
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:
simp

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

Goal state before:
pp: case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Tactic:
simp

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = f ≫ Cofork.π s ≫ i.hom

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

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

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝ : J
⊢ eqToHom ⋯ ≫ p j✝ = p j✝ ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = p j✝ ≫ 0

Tactic:
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 g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
j✝ : J
⊢ ι f j✝ ≫ map p ≫ desc k = ι f j✝ ≫ desc fun j ↦ p j ≫ k j

Tactic:
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 g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
j✝ : J
⊢ (lift k ≫ map p) ≫ π g j✝ = (lift fun j ↦ k j ≫ p j) ≫ π g j✝

Tactic:
simp

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

Goal state before:
pp: case isTrue
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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
j✝ : J
⊢ eqToHom ⋯ ≫ p j✝ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝

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

Goal state after: