mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 Y ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    𝟙 Y ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
⊢ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift a c ≫ σ = prod.lift a c ≫ σ

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift b d ≫ σ = prod.lift b d ≫ σ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
hvu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ b - (0 - a) = b - (0 - a)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - b = a - b

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - (a - b) = 0 - a + b

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - (a - b) = 0 - a + b
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯) ≫ F.m = kernel.ι (cokernel.π f)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯) ≫ F.m = kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - a - (0 - b) = 0 - a - (0 - b)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -a - b = -a - b

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m = coimageImageComparison f ≫ kernel.ι (cokernel.π f)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m = coimageImageComparison f ≫ kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - (b - c) = a - (b - c)

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (cokernel.π (kernel.ι f) ≫ coimageImageComparison f)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (cokernel.π (kernel.ι f) ≫ coimageImageComparison f)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + (b + c) = a + (b + c)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ prod.lift (f ≫ g) (f ≫ h) ≫ σ = prod.lift (f ≫ g) (f ≫ h) ≫ σ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ prod.lift (f ≫ h) (g ≫ h) ≫ σ = prod.lift (f ≫ h) (g ≫ h) ≫ σ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W✝ : C
w : W✝ ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
W : C
h : coequalizer u v ⟶ W
⊢ 0 ≫ h = 0 ≫ h

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ g = limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ g = limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f =
    (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ (KernelFork.ofι 0 ⋯).pt
hn : 0 = w
⊢ u = v

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ (KernelFork.ofι 0 ⋯).pt
hn : 0 = w
⊢ u = v
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
e_1✝ : (s.pt ⟶ Y✝) = (s.pt ⟶ (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5✝ : Y✝ = (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero = f

Tactic:
]

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
e_1✝ : (s.pt ⟶ Y✝) = (s.pt ⟶ (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5✝ : Y✝ = (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero = f
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ f ≫ inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A =
    f ≫ inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A

Tactic:
]

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

Goal state before:
pp: case e'_2.e'_6
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f

Tactic:
]

Goal state after:
case e'_2.e'_6
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ f = f

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ F.map i = F.map i

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ F.map p = F.map p

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.fst = s.ι ≫ biprod.fst

Tactic:
]

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.fst = s.ι ≫ biprod.fst
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.snd = s.ι ≫ biprod.snd

Tactic:
]

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.snd = s.ι ≫ biprod.snd
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.fst = s.ι ≫ biprod.fst

Tactic:
]

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.snd = s.ι ≫ biprod.snd

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ 0 = 0

Tactic:
]

Goal state after: