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
X Y : C
⊢ Function.LeftInverse ⋯ ⋯

Tactic:
cat_disch

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
⊢ Function.RightInverse ⋯ ⋯

Tactic:
cat_disch

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

Goal state before:
pp: case left_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.LeftInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.left_inv._autoParam

Tactic:
cat_disch

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

Goal state before:
pp: case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.RightInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.right_inv._autoParam

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
⊢ ∀ (a : ⊥_ C ⟶ X), a = default

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
⊢ ∀ (a : X ⟶ ⊤_ C), a = default

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F G : C ⥤ D
H : D ⥤ E
inst✝ : H.PreservesZeroMorphisms
⊢ whiskerRight 0 H = 0

Tactic:
cat_disch

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
⊢ inl ≫ snd X Y = 0

Tactic:
by
  simp [coprod.snd]

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 ≫ snd X Y = 𝟙 Y

Tactic:
by
  simp [coprod.snd]

Goal state after:
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
D : Type u'
F : D → C
X Y : InducedCategory C F
⊢ ∀ (m : R) (x : X ⟶ Y),
    InducedCategory.homAddEquiv.toFun (m • x) = (RingHom.id R) m • InducedCategory.homAddEquiv.toFun x

Tactic:
cat_disch

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)
i : IsLimit c
s : Fork f g
m✝ : s.pt ⟶ (forkOfKernelFork c).pt
h : m✝ ≫ (forkOfKernelFork c).ι = s.ι
⊢ m✝ ≫ Fork.ι c = i.lift (kernelForkOfFork s) ≫ Fork.ι c

Tactic:
cat_disch

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
i : IsLimit c
s : Fork (f - g) 0
m✝ : s.pt ⟶ (kernelForkOfFork c).pt
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = s.ι
⊢ m✝ ≫ c.ι = i.lift (forkOfKernelFork s) ≫ c.ι

Tactic:
cat_disch

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)
i : IsColimit c
s : Cofork f g
m✝ : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m✝ = s.π
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ i.desc (cokernelCoforkOfCofork s)

Tactic:
cat_disch

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
i : IsColimit c
s : Cofork (f - g) 0
m✝ : (cokernelCoforkOfCofork c).pt ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ i.desc (coforkOfCokernelCofork s)

Tactic:
cat_disch

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
q : Y ⟶ Y
w : f ≫ q = 𝟙 X ≫ f
⊢ map f f (𝟙 X) q w = 𝟙 (kernel f)

Tactic:
cat_disch

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' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ kernel.map f f' p q w ≫ kernel.lift f (kernel.ι f' ≫ inv p) ⋯ = 𝟙 (kernel f)

Tactic:
cat_disch

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' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ kernel.lift f (kernel.ι f' ≫ inv p) ⋯ ≫ kernel.map f f' p q w = 𝟙 (kernel f')

Tactic:
cat_disch

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 X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
inst✝¹ : HasKernel f
inst✝ : HasKernel f'
q : Y ⟶ Y'
w : f ≫ q = 0 ≫ f'
⊢ map f f' 0 q w = 0

Tactic:
cat_disch

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : Cofork f 0
⊢ s.ι.app zero ≫ (Iso.refl s.pt).hom = (Cofork.ofπ s.π ⋯).ι.app zero

Tactic:
cat_disch

Goal state after:
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
s : Cofork f 0
⊢ s.ι.app one ≫ (Iso.refl s.pt).hom = (Cofork.ofπ s.π ⋯).ι.app one

Tactic:
cat_disch

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ (CokernelCofork.ofπ π w).ι.app zero ≫ (Iso.refl (CokernelCofork.ofπ π w).pt).hom =
    (CokernelCofork.ofπ π' ⋯).ι.app zero

Tactic:
cat_disch

Goal state after:
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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ (CokernelCofork.ofπ π w).ι.app one ≫ (Iso.refl (CokernelCofork.ofπ π w).pt).hom = (CokernelCofork.ofπ π' ⋯).ι.app one

Tactic:
cat_disch

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
hf : f = 0
Z'✝ : C
x✝² : Y ⟶ Z'✝
x✝¹ : f ≫ x✝² = 0
x✝ : Y ⟶ Z'✝
hb : 𝟙 Y ≫ x✝ = x✝²
⊢ x✝ = x✝²

Tactic:
simp only [← hb, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝³ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : Epi p
inst✝ : IsIso q
⊢ cokernel.map f f' p q w ≫ cokernel.desc f' (inv q ≫ cokernel.π f) ⋯ = 𝟙 (cokernel f)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝³ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : Epi p
inst✝ : IsIso q
⊢ cokernel.desc f' (inv q ≫ cokernel.π f) ⋯ ≫ cokernel.map f f' p q w = 𝟙 (cokernel f')

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
q : X ⟶ X
w : f ≫ 𝟙 Y = q ≫ f
⊢ map f f q (𝟙 Y) w = 𝟙 (cokernel f)

Tactic:
cat_disch

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 X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
inst✝¹ : HasCokernel f
inst✝ : HasCokernel f'
q : X ⟶ X'
w : f ≫ 0 = q ≫ f'
⊢ map f f' q 0 w = 0

Tactic:
cat_disch

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
F : J → C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0

Tactic:
cat_disch

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁶ : Category.{uC', uC} C
inst✝⁵ : HasZeroMorphisms C
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J → C
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Bicone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.hom ≫ Y✝.π j) = G.map (X✝.π j)

Tactic:
by simpa using! t.wπ j

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁶ : Category.{uC', uC} C
inst✝⁵ : HasZeroMorphisms C
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J → C
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Bicone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
⊢ (functoriality F G).map { hom := G.preimage t.hom, wπ := ⋯, wι := ⋯ } = t

Tactic:
cat_disch

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w

Goal state after:
case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f 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✝
D : Type uD
inst✝⁶ : Category.{uD', uD} D
inst✝⁵ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi (map p)

Tactic:
have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc, ι_π_assoc]
    split
    · subst_vars
      simp
    · simp_all
  rw [this]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasKernels C
⊢ ι C ≫ Arrow.leftToRight = 0

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasCokernels C
⊢ Arrow.leftToRight ≫ π C = 0

Tactic:
cat_disch

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

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

Tactic:
← hf',

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

Goal state before:
pp: case pos
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
w : j = j'
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    0

Tactic:
cases w

Goal state after:
case pos.refl
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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x y : f j
h : j = j → ¬x ≍ y
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j, y⟩.fst ≫ biproduct.π (g ⟨j, y⟩.fst) ⟨j, y⟩.snd =
    0
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 : C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ (functoriality P Q F).map { hom := F.preimage t.hom, wfst := ⋯, wsnd := ⋯, winl := ⋯, winr := ⋯ } = t

Tactic:
cat_disch

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 P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ BinaryFan.fst ((Cone.postcompose (mapPairIso eP eQ).hom).obj b.toCone) =
    (Iso.refl ((Cone.postcompose (mapPairIso eP eQ).hom).obj b.toCone).pt).hom ≫ BinaryFan.fst (b.ofIso eP eQ).toCone

Tactic:
simp [BinaryFan.fst]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
⊢ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) = 𝟙 (⨁ f)

Tactic:
cases nonempty_fintype β
    ext g g'
    by_cases h : g' = g <;>
      simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        ← Equiv.eq_symm_apply, h]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).hom = prod.lift fst snd

Tactic:
ext <;> simp [biprod.isoProd]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoCoprod X Y).inv = coprod.desc inl inr

Tactic:
ext <;> simp [biprod.isoCoprod]

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {W' : C} (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 →
      ∀ (m : W' ⟶ ⨁ Subtype.restrict pᶜ f), m ≫ biproduct.fromSubtype f pᶜ = g' → m = g' ≫ biproduct.toSubtype f pᶜ

Tactic:
cat_disch

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {Z' : C} (g' : ⨁ f ⟶ Z'),
    biproduct.fromSubtype f p ≫ g' = 0 →
      ∀ (m : ⨁ Subtype.restrict pᶜ f ⟶ Z'), biproduct.toSubtype f pᶜ ≫ m = g' → m = biproduct.fromSubtype f pᶜ ≫ g'

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ braiding' P Q = braiding P Q

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ map f g ≫ (braiding Y W).hom = (braiding X Z).hom ≫ map g f

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
⊢ { app := fun M ↦ M.smul 1, naturality := ⋯ } = 1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (braiding X W).hom ≫ map f g ≫ (braiding Y Z).hom = map g f

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x✝¹ x✝ : R
⊢ { app := fun M ↦ M.smul (x✝¹ * x✝), naturality := ⋯ } =
    { app := fun M ↦ M.smul x✝¹, naturality := ⋯ } * { app := fun M ↦ M.smul x✝, naturality := ⋯ }

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ lift snd fst ≫ lift snd fst = 𝟙 (P ⊞ Q)

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
⊢ { app := fun M ↦ M.smul 0, naturality := ⋯ } = 0

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x✝¹ x✝ : R
⊢ { app := fun M ↦ M.smul (x✝¹ + x✝), naturality := ⋯ } =
    { app := fun M ↦ M.smul x✝¹, naturality := ⋯ } + { app := fun M ↦ M.smul x✝, naturality := ⋯ }

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
U V W X Y Z : C
f : U ⟶ X
g : V ⟶ Y
h : W ⟶ Z
⊢ map (map f g) h ≫ (associator X Y Z).hom = (associator U V W).hom ≫ map f (map g h)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
U V W X Y Z : C
f : U ⟶ X
g : V ⟶ Y
h : W ⟶ Z
⊢ map f (map g h) ≫ (associator X Y Z).inv = (associator U V W).inv ≫ map (map f g) h

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ Pi.Lex (fun x1 x2 ↦ x1 < x2) s (cons x₀ x) (cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i ↦ s) x y

Tactic:
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_iff_succ]

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨
      ∃ i,
        ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mp
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f) → f 0 + ∑ i, f i.succ = n

Tactic:
rintro ⟨a, b, rfl, g, rfl, rfl⟩

Goal state after:
case mp
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
d✝ d : ℕ
a : μ
g : Fin d → μ
⊢ Fin.cons a g 0 + ∑ i, Fin.cons a g i.succ = a + ∑ i, g i