mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
⊢ map m ≫ matrix n = matrix fun j k ↦ m j ≫ n j k

Tactic:
ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (map m ≫ matrix n) ≫ π h j✝¹ = ι f j✝ ≫ (matrix fun j k ↦ m j ≫ n j k) ≫ π h j✝¹
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

Goal state after:
case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.fst = inl ≫ prod.lift fst snd ≫ prod.fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.fst = inr ≫ prod.lift fst snd ≫ prod.fst

case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.snd = inl ≫ prod.lift fst snd ≫ prod.snd

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.snd = inr ≫ prod.lift fst snd ≫ prod.snd
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).inv = lift prod.fst prod.snd

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ fst = lift prod.fst prod.snd ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ snd = lift prod.fst prod.snd ≫ snd
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

Goal state after:
case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inl ≫ coprod.desc inl inr) ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inl ≫ coprod.desc inl inr) ≫ snd

case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inr ≫ coprod.desc inl inr) ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inr ≫ coprod.desc inl inr) ≫ snd
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
⊢ (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inl ≫ (biprod.isoCoprod X Y).hom = biprod.inl ≫ biprod.desc coprod.inl coprod.inr

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inr ≫ (biprod.isoCoprod X Y).hom = biprod.inr ≫ biprod.desc coprod.inl coprod.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = map' f g

Tactic:
ext

Goal state after:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ map' f g) ≫ fst

case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd

case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd
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
⊢ IsIso inl ↔ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
constructor

Goal state after:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl

case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl
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
⊢ fst ≫ inl + snd ≫ inr = 𝟙 (X ⊞ Y)

Tactic:
ext

Goal state after:
case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inl ≫ (fst ≫ inl + snd ≫ inr)) ≫ fst = (inl ≫ 𝟙 (X ⊞ Y)) ≫ fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inl ≫ (fst ≫ inl + snd ≫ inr)) ≫ snd = (inl ≫ 𝟙 (X ⊞ Y)) ≫ snd

case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inr ≫ (fst ≫ inl + snd ≫ inr)) ≫ fst = (inr ≫ 𝟙 (X ⊞ Y)) ≫ fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inr ≫ (fst ≫ inl + snd ≫ inr)) ≫ snd = (inr ≫ 𝟙 (X ⊞ Y)) ≫ snd
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
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g = f ≫ inl + g ≫ inr

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ fst = (f ≫ inl + g ≫ inr) ≫ fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ snd = (f ≫ inl + g ≫ inr) ≫ snd
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
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ desc f g = fst ≫ f + snd ≫ g

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ inl ≫ desc f g = inl ≫ (fst ≫ f + snd ≫ g)

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ inr ≫ desc f g = inr ≫ (fst ≫ f + snd ≫ g)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = fst ≫ f ≫ inl + snd ≫ g ≫ inr

Tactic:
ext

Goal state after:
case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ snd

case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
⊢ matrix m ≫ π g k = desc fun j ↦ m j k

Tactic:
ext

Goal state after:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ π g k = ι f j✝ ≫ desc fun j ↦ m j k
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
⊢ (matrix fun j k ↦ components m j k) = m

Tactic:
ext

Goal state after:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix fun j k ↦ components m j k) ≫ π g j✝¹ = ι f j✝ ≫ m ≫ π g 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✝
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
⊢ components (matrix m) = m

Tactic:
ext

Goal state after:
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✝
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
x✝¹ : J
x✝ : K
⊢ components (matrix m) x✝¹ x✝ = m x✝¹ x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ fst.op ≫ (opIso P Q).hom = inl

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ fst = inl ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ snd = inl ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ snd.op ≫ (opIso P Q).hom = inr

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ fst = inr ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ snd = inr ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (opIso P Q).inv ≫ inl.op = fst

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inl.op = inl ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inl.op = inr ≫ fst
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e ≫ ↟↑e.symm = 𝟙 (of R X₁)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₁)
⊢ (Hom.hom (↟↑e ≫ ↟↑e.symm)) x✝ = (Hom.hom (𝟙 (of R X₁))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e.symm ≫ ↟↑e = 𝟙 (of R X₂)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R X₂))) x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (opIso P Q).inv ≫ inr.op = snd

Tactic:
ext

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inr.op = inl ≫ snd

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inr.op = inr ≫ snd
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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ f default = f j

Tactic:
congr; rw [← Unique.uniq]

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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ f j = f default

Tactic:
congr; rw [← Unique.uniq]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) ↔ IsZero A ∧ IsZero B

Tactic:
constructor

Goal state after:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) → IsZero A ∧ IsZero B

case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝ M N : ModuleCat S
s₀ : S₀
f : x✝ ⟶ M
g : M ⟶ N
⊢ (s₀ • f) ≫ g = s₀ • f ≫ g

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝¹ M N : ModuleCat S
s₀ : S₀
f : x✝¹ ⟶ M
g : M ⟶ N
x✝ : ↑x✝¹
⊢ (Hom.hom ((s₀ • f) ≫ g)) x✝ = (Hom.hom (s₀ • f ≫ g)) x✝
Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso (biprod.map g f)

Tactic:
rw [← biprod.braiding_map_braiding]
    infer_instance

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ insertNthOrderIso α 0 = consOrderIso α

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
x✝¹ : α 0 × ((i : Fin n) → α (succAbove 0 i))
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso α 0) x✝¹ x✝ = (consOrderIso α) x✝¹ x✝
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝ : LE α
⊢ insertNthOrderIso (fun x ↦ α) (last n) = snocOrderIso fun x ↦ α

Tactic:
ext

Goal state after:
n : ℕ
α : Type u_2
inst✝ : LE α
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso (fun x ↦ α) (last n)) x✝¹ x✝ = (snocOrderIso fun x ↦ α) x✝¹ x✝
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f

Tactic:
ext

Goal state after:
case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inl ≫ f) ≫ biprod.fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inl ≫ f) ≫ biprod.snd

case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inr ≫ f) ≫ biprod.fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inr ≫ f) ≫ biprod.snd
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom =
    biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)

Tactic:
ext

Goal state after:
case h₀.h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (biprod.inl ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.fst =
    (biprod.inl ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.fst

case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (biprod.inl ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.snd =
    (biprod.inl ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.snd

case h₁.h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (biprod.inr ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.fst =
    (biprod.inr ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.fst

case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (biprod.inr ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.snd =
    (biprod.inr ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.snd
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (∀ x ∈ antidiagonal n, (map (fun x_1 ↦ Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup) ∧
    Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
      (antidiagonal n)

Tactic:
constructor

Goal state after:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ ∀ x ∈ antidiagonal n, (map (fun x_1 ↦ Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup

case succ.right
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)