mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)

Tactic:
]

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✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)
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 : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • g = r • g'
⊢ g = g'

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • g = r • g'
⊢ g = g'
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 : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : r • g = r • g'
⊢ g = g'

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : r • g = r • g'
⊢ g = g'
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✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : g = g'
⊢ g = g'

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : g = g'
⊢ g = g'
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✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g = g'
⊢ g = g'

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g = g'
⊢ g = g'
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✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f * 0 = 0

Tactic:
dsimp [mul]; exact HasZeroMorphisms.zero_comp _ f

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
a : P✝ ⟶ c.pt
ha : a ≫ Fork.ι c = g
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ 0 = 0

Tactic:
]

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
inst✝ : IsIso f
⊢ g = 0 ↔ g = 0

Tactic:
]

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
inst✝ : IsIso g
⊢ f = 0 ↔ f = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)

Tactic:
]

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')

Tactic:
]

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
a : α
⊢ P a ≤ (⨆ a, P a).isoClosure

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
a : α
⊢ P a ≤ (⨆ a, P a).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

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

Tactic:
]

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

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

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
s : KernelFork 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
Z : C
ι : Z ⟶ X
w : ι ≫ f = 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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (PreservesLimitPair.iso G X Y).hom

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (PreservesLimitPair.iso G X Y).hom
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (PreservesColimitPair.iso G X Y).hom

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (PreservesColimitPair.iso G X Y).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✝
X Y K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
⊢ k = k

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 : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
⊢ (s.ι ≫ f) ≫ g = (s.ι ≫ 0) ≫ g

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
⊢ (s.ι ≫ f) ≫ g = (s.ι ≫ 0) ≫ g
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 : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ m✝ ≫ Fork.ι c = ↑l ≫ Fork.ι c

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ m✝ ≫ Fork.ι c = ↑l ≫ Fork.ι c
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 : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ s.ι = ↑l ≫ Fork.ι c

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ s.ι = ↑l ≫ Fork.ι c
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 : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g
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
hf : f = 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✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork 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
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
⊢ 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 : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 0 = 0

Tactic:
]

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
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
]

Goal state after:
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
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case neg
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
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : ¬j = j'
⊢ 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✝² : HasKernel f✝
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ parallelPair g 0 ≅ parallelPair g 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✝² : 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:
]

Goal state after:
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
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
inst✝ : Mono f
s : Fork f 0
⊢ 0 = s.ι

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasZeroObject C
inst✝ : Mono f
s : Fork f 0
⊢ 0 = 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✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ 0 = 0

Tactic:
]

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
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ F.map (desc g) = F.map (desc g)

Tactic:
]

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
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) = F.map (lift f g)

Tactic:
]

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
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ F.map (desc f g) = F.map (desc f g)

Tactic:
]

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✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (PreservesProduct.iso G f).hom

Tactic:
]

Goal state after:
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✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (PreservesProduct.iso G f).hom
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:
]

Goal state after:
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
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✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (PreservesCoproduct.iso G f).inv

Tactic:
]

Goal state after:
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✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (PreservesCoproduct.iso G f).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
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
Z : C
π : Y ⟶ Z
w : f ≫ π = 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ 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 Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
⊢ k = k

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

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
⊢ (g ≫ f) ≫ Cofork.π c = 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
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:
]

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
⊢ 0 ≫ s.π = g ≫ 0 ≫ 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
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.π
⊢ Cofork.π c ≫ m✝ = 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.π
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ ↑l