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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (m : s.pt ⟶ (Fan.mk c.pt c.π.app).pt),
    (∀ (j : J), m ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j) →
      m = hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } }

Tactic:
by subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (j : J),
    (Cofan.mk c.pt c.ι.app).inj j ≫ hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } } = t.inj j

Tactic:
by subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (m : (Cofan.mk c.pt c.ι.app).pt ⟶ t.pt),
    (∀ (j : J), (Cofan.mk c.pt c.ι.app).inj j ≫ m = t.inj j) →
      m = hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } }

Tactic:
by subsingleton

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map (f ≫ coprod.inl)) (F.map (coprod.inr ≫ coprod.map f g)) =
    coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr))

Tactic:
coprod.inr_map

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)) =
    coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
s : BinaryCofan (op X) (op Y)
m : op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) ⟶ s.pt
h₁ : c.fst.op ≫ m = s.inl
h₂ : c.snd.op ≫ m = s.inr
⊢ m.unop ≫ c.snd = (hc.lift s.unop).op.unop ≫ c.snd

Tactic:
simp [← h₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
s : BinaryFan (op X) (op Y)
m : s.pt ⟶ op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h₁ : m ≫ c.inl.op = s.fst
h₂ : m ≫ c.inr.op = s.snd
⊢ c.inr ≫ m.unop = c.inr ≫ (hc.desc s.unop).op.unop

Tactic:
simp [← h₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
s : BinaryCofan X Y
m : unop (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) ⟶ s.pt
h₁ : c.fst.unop ≫ m = s.inl
h₂ : c.snd.unop ≫ m = s.inr
⊢ m.op ≫ c.snd = (hc.lift s.op).unop.op ≫ c.snd

Tactic:
simp [← h₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
s : BinaryFan X Y
m : s.pt ⟶ unop (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h₁ : m ≫ c.inl.unop = s.fst
h₂ : m ≫ c.inr.unop = s.snd
⊢ c.inr ≫ m.op = c.inr ≫ (hc.desc s.op).unop.op

Tactic:
simp [← h₂]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.left } = t.π.app { as := WalkingPair.swap WalkingPair.left }
⊢ m ≫ s.π.app { as := WalkingPair.left } = (BinaryFan.swap t).π.app { as := WalkingPair.left }

Tactic:
exact w

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.right } = t.π.app { as := WalkingPair.swap WalkingPair.right }
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.swap t).π.app { as := WalkingPair.right }

Tactic:
exact w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 none) ≫ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ g ≫ inr = (f ≫ inl) ≫ 𝟙 W

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
P : Over X → Prop
⊢ (∀ (Y : Over X), P Y) ↔ ∀ (Y : T) (f : Y ⟶ X), P (mk f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
P : Under X → Prop
⊢ (∀ (Y : Under X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (mk f)

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∀ (a : { as := PUnit.unit } ⟶ { as := PUnit.unit }), a = 𝟙 { as := PUnit.unit }

Tactic:
by subsingleton

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift { I := image ((f ≫ g) ≫ h), m := ι ((f ≫ g) ≫ h), m_mono := ⋯, e := factorThruImage ((f ≫ g) ≫ h), fac := ⋯ } ≫
      ι ((f ≫ g) ≫ h)

Tactic:
image.lift_fac

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) = ι (f ≫ g ≫ h)
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat R
i : X ≅ Y
⊢ Hom.hom i.hom ∘ₗ Hom.hom i.inv = LinearMap.id

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat R
i : X ≅ Y
⊢ Hom.hom i.inv ∘ₗ Hom.hom i.hom = LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
m : s.pt ⟶ t.pt
j : ∀ (j : WalkingParallelPair), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app zero = s.π.app zero

Tactic:
exact w

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

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
exact w

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

Goal state before:
pp: case mk.mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ { hom := hom✝, w := w✝ }.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Tactic:
aesop

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

Goal state before:
pp: case mk.mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ { hom := hom✝, w := w✝ }.hom = Cofork.π { pt := pt✝, ι := ι✝ }

Tactic:
aesop

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
i : IsIso 0
⊢ 0 ≫ inv 0 = 0 ∧ 𝟙 Y = 0

Tactic:
rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]

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
i : IsIso 0
⊢ 0 ≫ inv 0 = 0 ∧ inv 0 ≫ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    x ∈
      WalkingParallelPair.recOn j
        (WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset [left, right].toFinset)
        (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)

Tactic:
aesop

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

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

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X Y : C
hY : (⨆ a, P a) Y
e : X ≅ Y
⊢ (⨆ a, (P a).isoClosure) X
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
have := preservesSmallestColimits_of_preservesColimits F

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J 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
s : Fork f 0
⊢ ∀ (j : WalkingParallelPair), s.π.app j = (Iso.refl s.pt).hom ≫ (Fork.ofι s.ι ⋯).π.app j

Tactic:
aesop

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)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (G.mapCone (BinaryFan.mk prod.fst prod.snd))

Tactic:
apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _

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)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case zero.zero.id
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
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map (WalkingParallelPairHom.id zero) ≫ (app zero).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map (WalkingParallelPairHom.id zero)

Tactic:
aesop

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

Goal state before:
pp: case zero.one.left
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
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map WalkingParallelPairHom.left ≫ (app one).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map WalkingParallelPairHom.left

Tactic:
aesop

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

Goal state before:
pp: case zero.one.right
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
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map WalkingParallelPairHom.right ≫ (app one).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map WalkingParallelPairHom.right

Tactic:
aesop

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

Goal state before:
pp: case one.one.id
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
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map (WalkingParallelPairHom.id one) ≫ (app one).hom =
    (app one).hom ≫ (parallelPair (F.map f) 0).map (WalkingParallelPairHom.id one)

Tactic:
aesop

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:
exact w

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)
⊢ map p = (biproduct.isoProduct f).inv ≫ biproduct.map p ≫ (biproduct.isoProduct g).hom

Tactic:
aesop

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)
⊢ map p = (isoProduct f).hom ≫ Pi.map p ≫ (isoProduct g).inv

Tactic:
aesop

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)
⊢ map p = (biproduct.isoCoproduct f).inv ≫ biproduct.map p ≫ (biproduct.isoCoproduct g).hom

Tactic:
aesop

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
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ 𝟙 (F.obj x✝²) = 0

Tactic:
exact NatTrans.congr_app ((IsZero.iff_id_eq_zero _).1 hF) _

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

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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
as : WalkingPair
⊢ b.toBicone.toCone.π.app { as := as } = (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := as }

Tactic:
cases as

Goal state after:
case left
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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

case right
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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
as : WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := as } ≫ (Iso.refl b.toBicone.toCocone.pt).hom = b.toCocone.ι.app { as := as }

Tactic:
cases as

Goal state after:
case left
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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

case right
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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j, g j ≫ h j

Tactic:
simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

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

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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ map f g = (isoCoprod W X).hom ≫ coprod.map f g ≫ (isoCoprod Y Z).inv

Tactic:
aesop

Goal state after:
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
Z : C
f : Z ⟶ X ⊞ Y
⊢ f = (f ≫ fst) ≫ inl + (f ≫ snd) ≫ inr

Tactic:
aesop

Goal state after:
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
Z : C
f g : Z ⟶ X ⊞ Y
⊢ f = g ↔ f ≫ fst = g ≫ fst ∧ f ≫ snd = g ≫ snd

Tactic:
aesop

Goal state after:
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
Z : C
f : X ⊞ Y ⟶ Z
⊢ f = fst ≫ inl ≫ f + snd ≫ inr ≫ f

Tactic:
aesop

Goal state after:
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
Z : C
f g : X ⊞ Y ⟶ Z
⊢ f = g ↔ inl ≫ f = inl ≫ g ∧ inr ≫ f = inr ≫ g

Tactic:
aesop

Goal state after: