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
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
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m✝ = s.π
⊢ s.π = Cofork.π c ≫ ↑l

Tactic:
]

Goal state after:
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
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m✝ = s.π
⊢ s.π = Cofork.π c ≫ ↑l
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:
]

Goal state after:
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
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
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 = 0

Tactic:
]

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
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ 0 = 0

Tactic:
]

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:
]

Goal state after:
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
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)
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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:
]

Goal state after:
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
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
F : MonoFactorisation f
⊢ 0 = 0

Tactic:
]

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
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : image.ι f ≫ cokernel.π f = 0
⊢ image.ι f ≫ cokernel.π f = 0

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : image.ι f ≫ cokernel.π f = 0
⊢ image.ι f ≫ cokernel.π f = 0
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
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ 0 = 0

Tactic:
]

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0

Tactic:
]

Goal state after:
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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0).π.app j'

Tactic:
]

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0).π.app j'
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
s : Cofork f 0
⊢ 0 = 0

Tactic:
]

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
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0).ι.app j'

Tactic:
]

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0).ι.app j'
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
k k' : K
⊢ (if h : g k = g k' then eqToHom ⋯ else 0) = if h : k = k' then eqToHom ⋯ else 0

Tactic:
split_ifs with h h' h' <;> simp [Equiv.apply_eq_iff_eq g] at h h'

Goal state after:
case pos
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
k k' : K
h✝ : g k = g k'
h' h : k = k'
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
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
k k' : K
h✝ : g k = g k'
h' : ¬k = k'
h : k = k'
⊢ eqToHom ⋯ = 0

case pos
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
k k' : K
h' : k = k'
h : ¬k = k'
⊢ 0 = eqToHom ⋯

case neg
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
k k' : K
h' h : ¬k = k'
⊢ 0 = 0
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:
]

Goal state after:
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
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 : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ (if h : j✝ = j✝¹ then eqToHom ⋯ else 0) ≫ p j✝¹ = p j✝ ≫ if h : j✝ = j✝¹ then eqToHom ⋯ else 0

Tactic:
]

Goal state after:
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
⊢ (if h : j✝ = j✝¹ then eqToHom ⋯ else 0) ≫ p j✝¹ = p j✝ ≫ if h : j✝ = j✝¹ then eqToHom ⋯ else 0
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
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j

Tactic:
]

Goal state after:
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
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map p ≫ G.map g = G.map p ≫ G.map g

Tactic:
]

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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ 0 = 0

Tactic:
]

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
this : map p = (isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv
⊢ Epi ((isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv)

Tactic:
]

Goal state after:
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)
this : map p = (isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv
⊢ Epi ((isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv)
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map p ≫ G.map g = G.map p ≫ G.map g

Tactic:
]

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi ((biproduct.isoProduct f).inv ≫ biproduct.map p ≫ (biproduct.isoProduct g).hom)

Tactic:
]

Goal state after:
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)
⊢ Epi ((biproduct.isoProduct f).inv ≫ biproduct.map p ≫ (biproduct.isoProduct g).hom)
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ 0 = 0

Tactic:
]

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono ((isoProduct f).hom ≫ Pi.map p ≫ (isoProduct g).inv)

Tactic:
]

Goal state after:
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), Mono (p j)
⊢ Mono ((isoProduct f).hom ≫ Pi.map p ≫ (isoProduct g).inv)
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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono ((biproduct.isoCoproduct f).inv ≫ biproduct.map p ≫ (biproduct.isoCoproduct g).hom)

Tactic:
]

Goal state after:
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), Mono (p j)
⊢ Mono ((biproduct.isoCoproduct f).inv ≫ biproduct.map p ≫ (biproduct.isoCoproduct g).hom)
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (coequalizer.π f 0) ≫ G.map (cokernel.map f g p q hpq) = G.map q ≫ G.map (coequalizer.π g 0)

Tactic:
simp only [← G.map_comp]; exact G.congr_map (cokernel.π_desc _ _ _)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map f' + F.map g')

Tactic:
]

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

Goal state before:
pp: case neg
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
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = 0 ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

pp: case neg.h
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
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

pp: case neg.h
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
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
]

Goal state after:
case neg
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
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = 0 ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

case neg.h
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
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

case neg.h
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
j : J
h : ¬k = e j
⊢ e j ≠ k
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Category.{v_3, u_3} E
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : Preadditive E
F : C ⥤ D
G : D ⥤ E
inst✝² : G.Additive
inst✝¹ : (F ⋙ G).Additive
inst✝ : G.Faithful
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
⊢ G.map (F.map f₁) + G.map (F.map f₂) = G.map (F.map f₁) + G.map (F.map f₂)

Tactic:
]

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

Goal state before:
pp: case neg
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
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = 0 ≫ (w j).hom

pp: case neg.h
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
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

pp: case neg.h
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
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
]

Goal state after:
case neg
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
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = 0 ≫ (w j).hom

case neg.h
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
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

case neg.h
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
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j
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
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : HasZeroObject C
⊢ 0 = 0

Tactic:
]

Goal state after: