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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasCoproduct f
b : β
Z✝ : C
x✝¹ x✝ : f b ⟶ Z✝
e : Sigma.π f b ≫ x✝¹ = Sigma.π f b ≫ x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasCoproduct f
b : β
Z✝ : C
x✝¹ x✝ : f b ⟶ Z✝
e : Sigma.π f b ≫ x✝¹ = Sigma.π f b ≫ x✝
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ prod.inl X Y = x✝ ≫ prod.inl X Y
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ prod.inl X Y = x✝ ≫ prod.inl X Y
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ Y
e : x✝¹ ≫ prod.inr X Y = x✝ ≫ prod.inr X Y
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ Y
e : x✝¹ ≫ prod.inr X Y = x✝ ≫ prod.inr X Y
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ fst X Y = 𝟙 X

Tactic:
by
  simp [coprod.fst]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ fst X Y = 0

Tactic:
by
  simp [coprod.fst]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : X ⟶ Z✝
e : coprod.fst X Y ≫ x✝¹ = coprod.fst X Y ≫ x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : X ⟶ Z✝
e : coprod.fst X Y ≫ x✝¹ = coprod.fst X Y ≫ x✝
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : coprod.snd X Y ≫ x✝¹ = coprod.snd X Y ≫ x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : coprod.snd X Y ≫ x✝¹ = coprod.snd X Y ≫ x✝
⊢ x✝¹ = x✝
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:
simpa using

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:
simpa using

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.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toRightCancelMonoid M)

Tactic:
intro m₁ m₂ h

Goal state after:
M : Type u
m₁ m₂ : CancelMonoid M
h : m₁.toRightCancelMonoid = m₂.toRightCancelMonoid
⊢ m₁ = m₂
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
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m ≫ Fork.ι c = i.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι c

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m ≫ Fork.ι c = 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
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
m : W'✝ ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c = hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c

Tactic:
simpa using

Goal state after:
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
m : W'✝ ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c ≫ e.hom = 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
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ (Iso.refl X).hom ≫ g' = 0

Tactic:
simpa using

Goal state after:
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
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h✝ : l ≫ i.hom = f
s✝ : KernelFork f
hs : IsLimit s✝
s : Fork l 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι s✝) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s✝) ⋯) = s.ι
⊢ m ≫ Fork.ι s✝ = hs.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι s✝

Tactic:
simpa using

Goal state after:
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
m : s.pt ⟶ (KernelFork.ofι (Fork.ι s✝) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s✝) ⋯) = s.ι
⊢ m ≫ Fork.ι s✝ = 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
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ Cofork.π c ≫ m = Cofork.π c ≫ i.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ Cofork.π c ≫ m = 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
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
m : c.pt ⟶ Z'✝
hm : (e.hom ≫ Cofork.π c) ≫ m = s
⊢ Cofork.π c ≫ m = Cofork.π c ≫ hc.desc (ofπ (e.inv ≫ s) ⋯)

Tactic:
simpa using

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
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
m : c.pt ⟶ Z'✝
hm : (e.hom ≫ Cofork.π c) ≫ m = s
⊢ e.hom ≫ Cofork.π c ≫ m = 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
hc : IsColimit c
X' : C
f' : X' ⟶ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0
⊢ ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ (Iso.refl Y).hom ≫ φ = 0

Tactic:
simpa using

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
c : CokernelCofork f
hc : IsColimit c
X' : C
f' : X' ⟶ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0
⊢ ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 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
B : Bicone F
j : J
⊢ B.ι j ≫ B.π j = 𝟙 (F j)

Tactic:
simpa using

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j : J
⊢ B.ι j ≫ B.π j = 𝟙 (F 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
F : J → C
B : Bicone F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 0

Tactic:
simpa using

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
m : (CokernelCofork.ofπ 0 ⋯).pt ⟶ s.pt
x✝ : Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ m = s.π
⊢ m = 0

Tactic:
by
      apply HasZeroObject.from_zero_ext

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
m : (CokernelCofork.ofπ (Cofork.π s✝) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s✝) ⋯) ≫ m = s.π
⊢ Cofork.π s✝ ≫ m = Cofork.π s✝ ≫ hs.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
simpa using

Goal state after:
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
m : (CokernelCofork.ofπ (Cofork.π s✝) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s✝) ⋯) ≫ m = s.π
⊢ Cofork.π s✝ ≫ m = s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
K : Type w'
inst✝ : HasBiproductsOfShape K C
e : J ≃ K
F : J → C
h : LimitBicone (F ∘ ⇑e.symm)
c : Bicone (F ∘ ⇑e.symm)
hc : c.IsBilimit
⊢ LimitBicone F

Tactic:
simpa using

Goal state after:
J : Type w
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
K : Type w'
inst✝ : HasBiproductsOfShape K C
e : J ≃ K
F : J → C
h : LimitBicone (F ∘ ⇑e.symm)
c : Bicone (F ∘ ⇑e.symm)
hc : c.IsBilimit
⊢ LimitBicone F
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:
by 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
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
⊢ IsZero (F.obj 0)

Tactic:
by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
a✝ : j ∈ Finset.univ
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
a✝ : j ∈ Finset.univ
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
a✝ : j ∈ Finset.univ
⊢ (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
a✝ : j ∈ Finset.univ
⊢ b.π j ≫ b.ι j ≫ m = b.π j ≫ s.ι.app { as := j }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.fst = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.snd = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.fst = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.snd = s.π.app { as := WalkingPair.right }
⊢ m = m ≫ b.fst ≫ b.inl + m ≫ b.snd ≫ b.inr
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.inl ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.inr ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.inl ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.inr ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ b.inl ≫ m + b.snd ≫ b.inr ≫ m
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
j : K
h : ¬(p j)ᶜ
w :
  (g' ≫ biproduct.toSubtype f p) ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩ =
    0 ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩
⊢ g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j

Tactic:
simpa using

Goal state after:
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✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
j : K
h : ¬(p j)ᶜ
w :
  (g' ≫ biproduct.toSubtype f p) ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩ =
    0 ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩
⊢ 0 = g' ≫ biproduct.π f j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ m ≫ b.fst - f = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ m ≫ b.snd - g = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
j : K
h : ¬(p j)ᶜ
w :
  biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ biproduct.fromSubtype f p ≫ g' =
    biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ 0
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
simpa using

Goal state after:
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✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
j : K
h : ¬(p j)ᶜ
w :
  biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ biproduct.fromSubtype f p ≫ g' =
    biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ 0
⊢ 0 = biproduct.ι f j ≫ g'
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ m ≫ b.fst - f = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ m ≫ b.snd - g = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ m - f = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ m - g = 0