[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f
[PROOFSTEP]
simp [dite_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f
[PROOFSTEP]
simp [comp_dite]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
apply DMatrix.ext
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ ∀ (i : W✝.ι) (j : Z✝.ι), ((f ≫ g) ≫ h) i j = (f ≫ g ≫ h) i j
[PROOFSTEP]
intros
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ((f ≫ g) ≫ h) i✝ j✝ = (f ≫ g ≫ h) i✝ j✝
[PROOFSTEP]
simp_rw [Hom.comp, sum_comp, comp_sum, Category.assoc]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x : Y✝.ι, ∑ x_1 : X✝.ι, f i✝ x_1 ≫ g x_1 x ≫ h x j✝ = ∑ x : X✝.ι, ∑ j : Y✝.ι, f i✝ x ≫ g x j ≫ h j j✝
[PROOFSTEP]
rw [Finset.sum_comm]
  -- porting note: added because `DMatrix.ext` is not triggered automatically
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ 𝟙 M i i = 𝟙 (X M i)
[PROOFSTEP]
simp [id_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : i ≠ j
⊢ 𝟙 M i j = 0
[PROOFSTEP]
simp [id_apply, h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N : Mat_ C
⊢ AddCommGroup (M ⟶ N)
[PROOFSTEP]
change AddCommGroup (DMatrix M.ι N.ι _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N : Mat_ C
⊢ AddCommGroup (DMatrix M.ι N.ι fun i j => (fun i j => X M i ⟶ X N j) i j)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f f' : M ⟶ N
g : N ⟶ K
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f f' : M ⟶ N
g : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ ((f + f') ≫ g) i✝ j✝ = (f ≫ g + f' ≫ g) i✝ j✝
[PROOFSTEP]
simp [Finset.sum_add_distrib]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f : M ⟶ N
g g' : N ⟶ K
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
ext
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f : M ⟶ N
g g' : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ (f ≫ (g + g')) i✝ j✝ = (f ≫ g + f ≫ g') i✝ j✝
[PROOFSTEP]
simp [Finset.sum_add_distrib]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
y : (f j).ι
⊢ (fun i j_1 => X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) i ⟶ X (f j) j_1) x y
[PROOFSTEP]
refine' if h : x.1 = j then _ else 0
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
y : (f j).ι
h : x.fst = j
⊢ (fun i j_1 => X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) i ⟶ X (f j) j_1) x y
[PROOFSTEP]
refine' if h' : @Eq.ndrec (Fin n) x.1 (fun j => (f j).ι) x.2 _ h = y then _ else 0
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
y : (f j).ι
h : x.fst = j
h' : h ▸ x.snd = y
⊢ (fun i j_1 => X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) i ⟶ X (f j) j_1) x y
[PROOFSTEP]
apply eqToHom
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
y : (f j).ι
h : x.fst = j
h' : h ▸ x.snd = y
⊢ X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y
[PROOFSTEP]
substs h h'
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
x : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
⊢ X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f x.fst) ((_ : x.fst = x.fst) ▸ x.snd)
[PROOFSTEP]
rfl
  -- Notice we were careful not to use `subst` until we had a goal in `Prop`.
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
⊢ (fun i j_1 => X (f j) i ⟶ X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) j_1) x y
[PROOFSTEP]
refine' if h : y.1 = j then _ else 0
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
h : y.fst = j
⊢ (fun i j_1 => X (f j) i ⟶ X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) j_1) x y
[PROOFSTEP]
refine' if h' : @Eq.ndrec _ y.1 (fun j => (f j).ι) y.2 _ h = x then _ else 0
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
h : y.fst = j
h' : h ▸ y.snd = x
⊢ (fun i j_1 => X (f j) i ⟶ X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) j_1) x y
[PROOFSTEP]
apply eqToHom
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
h : y.fst = j
h' : h ▸ y.snd = x
⊢ X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y
[PROOFSTEP]
substs h h'
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
y : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι
⊢ X (f y.fst) ((_ : y.fst = y.fst) ▸ y.snd) = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
⊢ (fun j x y =>
          if h : y.fst = j then
            if h' : h ▸ y.snd = x then
              eqToHom (_ : X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y)
            else 0
          else 0)
        j ≫
      (fun j x y =>
          if h : x.fst = j then
            if h' : h ▸ x.snd = y then
              eqToHom (_ : X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y)
            else 0
          else 0)
        j' =
    if h : j = j' then eqToHom (_ : f j = f j') else 0
[PROOFSTEP]
ext x y
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ ((fun j x y =>
            if h : y.fst = j then
              if h' : h ▸ y.snd = x then
                eqToHom (_ : X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y)
              else 0
            else 0)
          j ≫
        (fun j x y =>
            if h : x.fst = j then
              if h' : h ▸ x.snd = y then
                eqToHom (_ : X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y)
              else 0
            else 0)
          j')
      x y =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
dsimp
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ j_1 : (j : Fin n) × (f j).ι,
      (if h : j_1.fst = j then if h' : h ▸ j_1.snd = x then eqToHom (_ : X (f j) x = X (f j_1.fst) j_1.snd) else 0
        else 0) ≫
        if h : j_1.fst = j' then if h' : h ▸ j_1.snd = y then eqToHom (_ : X (f j_1.fst) j_1.snd = X (f j') y) else 0
        else 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
simp_rw [dite_comp, comp_dite]
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1 : (j : Fin n) × (f j).ι,
      if h : x_1.fst = j then
        if h_1 : (_ : x_1.fst = j) ▸ x_1.snd = x then
          if h_2 : x_1.fst = j' then
            if h_3 : (_ : x_1.fst = j') ▸ x_1.snd = y then
              eqToHom (_ : X (f j) x = X (f x_1.fst) x_1.snd) ≫ eqToHom (_ : X (f x_1.fst) x_1.snd = X (f j') y)
            else eqToHom (_ : X (f j) x = X (f x_1.fst) x_1.snd) ≫ 0
          else eqToHom (_ : X (f j) x = X (f x_1.fst) x_1.snd) ≫ 0
        else
          if h : x_1.fst = j' then
            if h_2 : (_ : x_1.fst = j') ▸ x_1.snd = y then 0 ≫ eqToHom (_ : X (f x_1.fst) x_1.snd = X (f j') y)
            else 0 ≫ 0
          else 0 ≫ 0
      else
        if h : x_1.fst = j' then
          if h_1 : (_ : x_1.fst = j') ▸ x_1.snd = y then 0 ≫ eqToHom (_ : X (f x_1.fst) x_1.snd = X (f j') y) else 0 ≫ 0
        else 0 ≫ 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
simp only [ite_self, dite_eq_ite, dif_ctx_congr, Limits.comp_zero, Limits.zero_comp, eqToHom_trans, Finset.sum_congr]
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1 : (j : Fin n) × (f j).ι,
      if h : x_1.fst = j then
        if h_1 : (_ : x_1.fst = j) ▸ x_1.snd = x then
          if h_2 : x_1.fst = j' then
            if h_3 : (_ : x_1.fst = j') ▸ x_1.snd = y then eqToHom (_ : X (f j) x = X (f j') y) else 0
          else 0
        else 0
      else 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
erw [Finset.sum_sigma]
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a : Fin n,
      ∑ s in (fun x => Finset.univ) a,
        if h : { fst := a, snd := s }.fst = j then
          if h_1 : (_ : { fst := a, snd := s }.fst = j) ▸ { fst := a, snd := s }.snd = x then
            if h_2 : { fst := a, snd := s }.fst = j' then
              if h_3 : (_ : { fst := a, snd := s }.fst = j') ▸ { fst := a, snd := s }.snd = y then
                eqToHom (_ : X (f j) x = X (f j') y)
              else 0
            else 0
          else 0
        else 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
dsimp
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a : Fin n,
      ∑ s : (f a).ι,
        if h : a = j then
          if h_1 : (_ : a = j) ▸ s = x then
            if h_2 : a = j' then if h_3 : (_ : a = j') ▸ s = y then eqToHom (_ : X (f j) x = X (f j') y) else 0 else 0
          else 0
        else 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
simp only [if_congr, if_true, dif_ctx_congr, Finset.sum_dite_irrel, Finset.mem_univ, Finset.sum_const_zero,
  Finset.sum_congr, Finset.sum_dite_eq']
[GOAL]
case H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (if h : j = j' then if h_1 : (_ : j = j') ▸ x = y then eqToHom (_ : X (f j) x = X (f j') y) else 0 else 0) =
    dite (j = j') (fun h => eqToHom (_ : f j = f j')) (fun h => 0) x y
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : (_ : j = j') ▸ x = y
⊢ eqToHom (_ : X (f j) x = X (f j') y) = eqToHom (_ : f j = f j') x y
[PROOFSTEP]
substs h h'
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
⊢ eqToHom (_ : X (f j) x = X (f j) ((_ : j = j) ▸ x)) = eqToHom (_ : f j = f j) x ((_ : j = j) ▸ x)
[PROOFSTEP]
simp only [CategoryTheory.eqToHom_refl, CategoryTheory.Mat_.id_apply_self]
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : ¬(_ : j = j') ▸ x = y
⊢ 0 = eqToHom (_ : f j = f j') x y
[PROOFSTEP]
subst h
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x y : (f j).ι
h' : ¬(_ : j = j) ▸ x = y
⊢ 0 = eqToHom (_ : f j = f j) x y
[PROOFSTEP]
rw [eqToHom_refl, id_apply_of_ne _ _ _ h']
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : ¬j = j'
⊢ 0 = OfNat.ofNat 0 x y
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ ∑ j : Fin n,
      Bicone.π
          (Bicone.mk (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd)
            (fun j x y =>
              if h : x.fst = j then
                if h' : h ▸ x.snd = y then
                  eqToHom (_ : X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y)
                else 0
              else 0)
            fun j x y =>
            if h : y.fst = j then
              if h' : h ▸ y.snd = x then
                eqToHom (_ : X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y)
              else 0
            else 0)
          j ≫
        Bicone.ι
          (Bicone.mk (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd)
            (fun j x y =>
              if h : x.fst = j then
                if h' : h ▸ x.snd = y then
                  eqToHom (_ : X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y)
                else 0
              else 0)
            fun j x y =>
            if h : y.fst = j then
              if h' : h ▸ y.snd = x then
                eqToHom (_ : X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y)
              else 0
            else 0)
          j =
    𝟙
      (Bicone.mk (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd)
          (fun j x y =>
            if h : x.fst = j then
              if h' : h ▸ x.snd = y then
                eqToHom (_ : X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) x = X (f j) y)
              else 0
            else 0)
          fun j x y =>
          if h : y.fst = j then
            if h' : h ▸ y.snd = x then
              eqToHom (_ : X (f j) x = X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) y)
            else 0
          else 0).pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ (∑ j : Fin n,
      (fun x y =>
          if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom (_ : X (f x.fst) x.snd = X (f j) y) else 0 else 0) ≫
        fun x y =>
        if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom (_ : X (f j) x = X (f y.fst) y.snd) else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd)
[PROOFSTEP]
ext1 ⟨i, j⟩
[GOAL]
case H.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
⊢ ∀ (j_1 : (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd).ι),
    Finset.sum Finset.univ
        (fun j =>
          (fun x y =>
              if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom (_ : X (f x.fst) x.snd = X (f j) y) else 0
              else 0) ≫
            fun x y =>
            if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom (_ : X (f j) x = X (f y.fst) y.snd) else 0 else 0)
        { fst := i, snd := j } j_1 =
      𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } j_1
[PROOFSTEP]
rintro ⟨i', j'⟩
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ Finset.sum Finset.univ
      (fun j =>
        (fun x y =>
            if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom (_ : X (f x.fst) x.snd = X (f j) y) else 0
            else 0) ≫
          fun x y =>
          if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom (_ : X (f j) x = X (f y.fst) y.snd) else 0 else 0)
      { fst := i, snd := j } { fst := i', snd := j' } =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
[PROOFSTEP]
rw [Finset.sum_apply, Finset.sum_apply]
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∑ c : Fin n,
      ((fun x y =>
            if h : x.fst = c then if h' : h ▸ x.snd = y then eqToHom (_ : X (f x.fst) x.snd = X (f c) y) else 0
            else 0) ≫
          fun x y =>
          if h : y.fst = c then if h' : h ▸ y.snd = x then eqToHom (_ : X (f c) x = X (f y.fst) y.snd) else 0 else 0)
        { fst := i, snd := j } { fst := i', snd := j' } =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
[PROOFSTEP]
dsimp
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ c : Fin n,
      ∑ j_1 : (f c).ι,
        (if h : i = c then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f c) j_1) else 0 else 0) ≫
          if h : i' = c then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f c) j_1 = X (f i') j') else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
[PROOFSTEP]
rw [Finset.sum_eq_single i]
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1 : (f i).ι,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f i) j_1) else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f i) j_1 = X (f i') j') else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ (b : Fin n),
    b ∈ Finset.univ →
      b ≠ i →
        (∑ j_1 : (f b).ι,
            (if h : i = b then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f b) j_1) else 0 else 0) ≫
              if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f b) j_1 = X (f i') j') else 0 else 0) =
          0
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ¬i ∈ Finset.univ →
    (∑ j_1 : (f i).ι,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f i) j_1) else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f i) j_1 = X (f i') j') else 0 else 0) =
      0
[PROOFSTEP]
rotate_left
[GOAL]
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ (b : Fin n),
    b ∈ Finset.univ →
      b ≠ i →
        (∑ j_1 : (f b).ι,
            (if h : i = b then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f b) j_1) else 0 else 0) ≫
              if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f b) j_1 = X (f i') j') else 0 else 0) =
          0
[PROOFSTEP]
intro b _ hb
[GOAL]
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ (∑ j_1 : (f b).ι,
      (if h : i = b then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f b) j_1) else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f b) j_1 = X (f i') j') else 0 else 0) =
    0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case H.mk.mk.h₀.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ∀ (x : (f b).ι),
    x ∈ Finset.univ →
      ((if h : i = b then if h' : h ▸ j = x then eqToHom (_ : X (f i) j = X (f b) x) else 0 else 0) ≫
          if h : i' = b then if h' : h ▸ j' = x then eqToHom (_ : X (f b) x = X (f i') j') else 0 else 0) =
        0
[PROOFSTEP]
intro x _
[GOAL]
case H.mk.mk.h₀.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝¹ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
a✝ : x ∈ Finset.univ
⊢ ((if h : i = b then if h' : h ▸ j = x then eqToHom (_ : X (f i) j = X (f b) x) else 0 else 0) ≫
      if h : i' = b then if h' : h ▸ j' = x then eqToHom (_ : X (f b) x = X (f i') j') else 0 else 0) =
    0
[PROOFSTEP]
rw [dif_neg hb.symm, zero_comp]
[GOAL]
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ¬i ∈ Finset.univ →
    (∑ j_1 : (f i).ι,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f i) j_1) else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f i) j_1 = X (f i') j') else 0 else 0) =
      0
[PROOFSTEP]
intro hi
[GOAL]
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
hi : ¬i ∈ Finset.univ
⊢ (∑ j_1 : (f i).ι,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f i) j_1) else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f i) j_1 = X (f i') j') else 0 else 0) =
    0
[PROOFSTEP]
simp at hi 
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1 : (f i).ι,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom (_ : X (f i) j = X (f i) j_1) else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom (_ : X (f i) j_1 = X (f i') j') else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
[PROOFSTEP]
rw [Finset.sum_eq_single j]
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom (_ : X (f i) j = X (f i) j) else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ (b : (f i).ι),
    b ∈ Finset.univ →
      b ≠ j →
        ((if h : i = i then if h' : h ▸ j = b then eqToHom (_ : X (f i) j = X (f i) b) else 0 else 0) ≫
            if h : i' = i then if h' : h ▸ j' = b then eqToHom (_ : X (f i) b = X (f i') j') else 0 else 0) =
          0
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ¬j ∈ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom (_ : X (f i) j = X (f i) j) else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
      0
[PROOFSTEP]
rotate_left
[GOAL]
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ (b : (f i).ι),
    b ∈ Finset.univ →
      b ≠ j →
        ((if h : i = i then if h' : h ▸ j = b then eqToHom (_ : X (f i) j = X (f i) b) else 0 else 0) ≫
            if h : i' = i then if h' : h ▸ j' = b then eqToHom (_ : X (f i) b = X (f i') j') else 0 else 0) =
          0
[PROOFSTEP]
intro b _ hb
[GOAL]
case H.mk.mk.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ((if h : i = i then if h' : h ▸ j = b then eqToHom (_ : X (f i) j = X (f i) b) else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = b then eqToHom (_ : X (f i) b = X (f i') j') else 0 else 0) =
    0
[PROOFSTEP]
rw [dif_pos rfl, dif_neg, zero_comp]
[GOAL]
case H.mk.mk.h₀.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ¬(_ : i = i) ▸ j = b
[PROOFSTEP]
simp only
[GOAL]
case H.mk.mk.h₀.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ¬j = b
[PROOFSTEP]
tauto
[GOAL]
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ¬j ∈ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom (_ : X (f i) j = X (f i) j) else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
      0
[PROOFSTEP]
intro hj
[GOAL]
case H.mk.mk.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
hj : ¬j ∈ Finset.univ
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom (_ : X (f i) j = X (f i) j) else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    0
[PROOFSTEP]
simp at hj 
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom (_ : X (f i) j = X (f i) j) else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    𝟙 (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } { fst := i', snd := j' }
[PROOFSTEP]
simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp, ne_eq, Sigma.mk.inj_iff, not_and, id_def]
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    if h : i = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
by_cases i' = i
[GOAL]
case H.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    if h : i = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
by_cases i' = i
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : i' = i
⊢ (if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    if h : i = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h : i' = i' then if h' : h ▸ j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0 else 0) =
    if h : i' = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
rw [dif_pos rfl]
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h' : (_ : i' = i') ▸ j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0) =
    if h : i' = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
simp only [heq_eq_eq, true_and]
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h' : j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0) =
    if h : j = j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
by_cases j' = j
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h' : j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0) =
    if h : j = j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
by_cases j' = j
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : j' = j
⊢ (if h' : j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0) =
    if h : j = j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' : (f i').ι
⊢ (if h' : j' = j' then eqToHom (_ : X (f i') j' = X (f i') j') else 0) =
    if h : j' = j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom (_ : X (f i') j = X (f i') j') else 0) =
    if h : j = j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
rw [dif_neg h, dif_neg (Ne.symm h)]
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ (if h : i' = i then if h' : h ▸ j' = j then eqToHom (_ : X (f i) j = X (f i') j') else 0 else 0) =
    if h : i = i' ∧ HEq j j' then
      eqToHom
        (_ :
          X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i, snd := j } =
            X (mk ((j : Fin n) × (f j).ι) fun p => X (f p.fst) p.snd) { fst := i', snd := j' })
    else 0
[PROOFSTEP]
rw [dif_neg h, dif_neg]
[GOAL]
case neg.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ ¬(i = i' ∧ HEq j j')
[PROOFSTEP]
tauto
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
M : Mat_ C
⊢ (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M
[PROOFSTEP]
cases M
[GOAL]
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (mapMat_ (𝟭 C)).obj (Mat_.mk ι✝ X✝) = (𝟭 (Mat_ C)).obj (Mat_.mk ι✝ X✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
M N : Mat_ C
f : M ⟶ N
⊢ (mapMat_ (𝟭 C)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) N).hom =
    ((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) M).hom ≫ (𝟭 (Mat_ C)).map f
[PROOFSTEP]
ext
[GOAL]
case H
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
M N : Mat_ C
f : M ⟶ N
i✝ : ((mapMat_ (𝟭 C)).obj M).ι
j✝ : ((𝟭 (Mat_ C)).obj N).ι
⊢ ((mapMat_ (𝟭 C)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) N).hom) i✝ j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) M).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝
[PROOFSTEP]
cases M
[GOAL]
case H.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
N : Mat_ C
j✝ : ((𝟭 (Mat_ C)).obj N).ι
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
f : Mat_.mk ι✝ X✝ ⟶ N
i✝ : ((mapMat_ (𝟭 C)).obj (Mat_.mk ι✝ X✝)).ι
⊢ ((mapMat_ (𝟭 C)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) N).hom) i✝ j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) (Mat_.mk ι✝ X✝)).hom ≫ (𝟭 (Mat_ C)).map f) i✝
      j✝
[PROOFSTEP]
cases N
[GOAL]
case H.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
ι✝¹ : Type
F✝¹ : Fintype ι✝¹
X✝¹ : ι✝¹ → C
i✝ : ((mapMat_ (𝟭 C)).obj (Mat_.mk ι✝¹ X✝¹)).ι
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
j✝ : ((𝟭 (Mat_ C)).obj (Mat_.mk ι✝ X✝)).ι
f : Mat_.mk ι✝¹ X✝¹ ⟶ Mat_.mk ι✝ X✝
⊢ ((mapMat_ (𝟭 C)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) (Mat_.mk ι✝ X✝)).hom) i✝
      j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (𝟭 C)).obj M = (𝟭 (Mat_ C)).obj M)) (Mat_.mk ι✝¹ X✝¹)).hom ≫ (𝟭 (Mat_ C)).map f)
      i✝ j✝
[PROOFSTEP]
simp [comp_dite, dite_comp]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
M : Mat_ C
⊢ (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M
[PROOFSTEP]
cases M
[GOAL]
case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (mapMat_ (F ⋙ G)).obj (Mat_.mk ι✝ X✝) = (mapMat_ F ⋙ mapMat_ G).obj (Mat_.mk ι✝ X✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
M N : Mat_ C
f : M ⟶ N
⊢ (mapMat_ (F ⋙ G)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) N).hom =
    ((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) M).hom ≫
      (mapMat_ F ⋙ mapMat_ G).map f
[PROOFSTEP]
ext
[GOAL]
case H
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
M N : Mat_ C
f : M ⟶ N
i✝ : ((mapMat_ (F ⋙ G)).obj M).ι
j✝ : ((mapMat_ F ⋙ mapMat_ G).obj N).ι
⊢ ((mapMat_ (F ⋙ G)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) N).hom)
      i✝ j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) M).hom ≫
        (mapMat_ F ⋙ mapMat_ G).map f)
      i✝ j✝
[PROOFSTEP]
cases M
[GOAL]
case H.mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
N : Mat_ C
j✝ : ((mapMat_ F ⋙ mapMat_ G).obj N).ι
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
f : Mat_.mk ι✝ X✝ ⟶ N
i✝ : ((mapMat_ (F ⋙ G)).obj (Mat_.mk ι✝ X✝)).ι
⊢ ((mapMat_ (F ⋙ G)).map f ≫ ((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) N).hom)
      i✝ j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) (Mat_.mk ι✝ X✝)).hom ≫
        (mapMat_ F ⋙ mapMat_ G).map f)
      i✝ j✝
[PROOFSTEP]
cases N
[GOAL]
case H.mk.mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : Additive F
G : D ⥤ E
inst✝ : Additive G
ι✝¹ : Type
F✝¹ : Fintype ι✝¹
X✝¹ : ι✝¹ → C
i✝ : ((mapMat_ (F ⋙ G)).obj (Mat_.mk ι✝¹ X✝¹)).ι
ι✝ : Type
F✝ : Fintype ι✝
X✝ : ι✝ → C
j✝ : ((mapMat_ F ⋙ mapMat_ G).obj (Mat_.mk ι✝ X✝)).ι
f : Mat_.mk ι✝¹ X✝¹ ⟶ Mat_.mk ι✝ X✝
⊢ ((mapMat_ (F ⋙ G)).map f ≫
        ((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) (Mat_.mk ι✝ X✝)).hom)
      i✝ j✝ =
    (((fun M => eqToIso (_ : (mapMat_ (F ⋙ G)).obj M = (mapMat_ F ⋙ mapMat_ G).obj M)) (Mat_.mk ι✝¹ X✝¹)).hom ≫
        (mapMat_ F ⋙ mapMat_ G).map f)
      i✝ j✝
[PROOFSTEP]
simp [comp_dite, dite_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
⊢ { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map (𝟙 x✝) =
    𝟙 ({ obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.obj x✝)
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case H.unit
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
j✝ : ({ obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.obj x✝).ι
⊢ { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map (𝟙 x✝) PUnit.unit j✝ =
    𝟙 ({ obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.obj x✝) PUnit.unit j✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map (x✝¹ ≫ x✝) =
    { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map x✝¹ ≫
      { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map x✝
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case H.unit
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
j✝ : ({ obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.obj Z✝).ι
⊢ { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map (x✝¹ ≫ x✝) PUnit.unit j✝ =
    ({ obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map x✝¹ ≫
        { obj := fun X => mk PUnit fun x => X, map := fun {X Y} f x x => f }.map x✝)
      PUnit.unit j✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ((biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
      biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) =
    𝟙 M
[PROOFSTEP]
simp only [biproduct.lift_desc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ (∑ j : M.ι,
      (fun j_1 k => if h : j_1 = j then eqToHom (_ : X M j_1 = X M j) else 0) ≫ fun j_1 k =>
        if h : j = k then eqToHom (_ : X M j = X M k) else 0) =
    𝟙 M
[PROOFSTEP]
funext i j
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ Finset.sum Finset.univ
      (fun j =>
        (fun j_1 k => if h : j_1 = j then eqToHom (_ : X M j_1 = X M j) else 0) ≫ fun j_1 k =>
          if h : j = k then eqToHom (_ : X M j = X M k) else 0)
      i j =
    𝟙 M i j
[PROOFSTEP]
dsimp [id_def]
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ Finset.sum Finset.univ
      (fun j =>
        (fun j_1 k => if h : j_1 = j then eqToHom (_ : X M j_1 = X M j) else 0) ≫ fun j_1 k =>
          if h : j = k then eqToHom (_ : X M j = X M k) else 0)
      i j =
    if h : i = j then eqToHom (_ : X M i = X M j) else 0
[PROOFSTEP]
rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫ fun j k =>
        if h : i = k then eqToHom (_ : X M i = X M k) else 0)
      i j =
    if h : i = j then eqToHom (_ : X M i = X M j) else 0
case h.h.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ (b : M.ι),
    b ∈ Finset.univ →
      b ≠ i →
        ((fun j k => if h : j = b then eqToHom (_ : X M j = X M b) else 0) ≫ fun j k =>
              if h : b = k then eqToHom (_ : X M b = X M k) else 0)
            i j =
          0
case h.h.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ¬i ∈ Finset.univ →
    ((fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫ fun j k =>
          if h : i = k then eqToHom (_ : X M i = X M k) else 0)
        i j =
      0
[PROOFSTEP]
rotate_left
[GOAL]
case h.h.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ (b : M.ι),
    b ∈ Finset.univ →
      b ≠ i →
        ((fun j k => if h : j = b then eqToHom (_ : X M j = X M b) else 0) ≫ fun j k =>
              if h : b = k then eqToHom (_ : X M b = X M k) else 0)
            i j =
          0
[PROOFSTEP]
intro b _ hb
[GOAL]
case h.h.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ((fun j k => if h : j = b then eqToHom (_ : X M j = X M b) else 0) ≫ fun j k =>
        if h : b = k then eqToHom (_ : X M b = X M k) else 0)
      i j =
    0
[PROOFSTEP]
dsimp
[GOAL]
case h.h.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ (∑ j_1 in {PUnit.unit},
      (if h : i = b then eqToHom (_ : X M i = X M b) else 0) ≫ if h : b = j then eqToHom (_ : X M b = X M j) else 0) =
    0
[PROOFSTEP]
simp only [Finset.sum_const, Finset.card_singleton, one_smul]
[GOAL]
case h.h.h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ((if h : i = b then eqToHom (_ : X M i = X M b) else 0) ≫ if h : b = j then eqToHom (_ : X M b = X M j) else 0) = 0
[PROOFSTEP]
rw [dif_neg hb.symm, zero_comp]
[GOAL]
case h.h.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ¬i ∈ Finset.univ →
    ((fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫ fun j k =>
          if h : i = k then eqToHom (_ : X M i = X M k) else 0)
        i j =
      0
[PROOFSTEP]
intro h
[GOAL]
case h.h.h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : ¬i ∈ Finset.univ
⊢ ((fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫ fun j k =>
        if h : i = k then eqToHom (_ : X M i = X M k) else 0)
      i j =
    0
[PROOFSTEP]
simp at h 
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫ fun j k =>
        if h : i = k then eqToHom (_ : X M i = X M k) else 0)
      i j =
    if h : i = j then eqToHom (_ : X M i = X M j) else 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ((biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) ≫
      biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) =
    𝟙 (⨁ fun i => (embedding C).obj (X M i))
[PROOFSTEP]
apply biproduct.hom_ext
[GOAL]
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ∀ (j : M.ι),
    ((biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) ≫
          biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
        biproduct.π (fun i => (embedding C).obj (X M i)) j =
      𝟙 (⨁ fun i => (embedding C).obj (X M i)) ≫ biproduct.π (fun i => (embedding C).obj (X M i)) j
[PROOFSTEP]
intro i
[GOAL]
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ ((biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) ≫
        biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
      biproduct.π (fun i => (embedding C).obj (X M i)) i =
    𝟙 (⨁ fun i => (embedding C).obj (X M i)) ≫ biproduct.π (fun i => (embedding C).obj (X M i)) i
[PROOFSTEP]
apply biproduct.hom_ext'
[GOAL]
case w.w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ ∀ (j : M.ι),
    biproduct.ι (fun i => (embedding C).obj (X M i)) j ≫
        ((biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) ≫
            biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
          biproduct.π (fun i => (embedding C).obj (X M i)) i =
      biproduct.ι (fun i => (embedding C).obj (X M i)) j ≫
        𝟙 (⨁ fun i => (embedding C).obj (X M i)) ≫ biproduct.π (fun i => (embedding C).obj (X M i)) i
[PROOFSTEP]
intro j
[GOAL]
case w.w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ biproduct.ι (fun i => (embedding C).obj (X M i)) j ≫
      ((biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) ≫
          biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
        biproduct.π (fun i => (embedding C).obj (X M i)) i =
    biproduct.ι (fun i => (embedding C).obj (X M i)) j ≫
      𝟙 (⨁ fun i => (embedding C).obj (X M i)) ≫ biproduct.π (fun i => (embedding C).obj (X M i)) i
[PROOFSTEP]
simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc, biproduct.ι_π]
[GOAL]
case w.w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j_1 k => if h : j = k then eqToHom (_ : X M j = X M k) else 0) ≫ fun j k =>
      if h : j = i then eqToHom (_ : X M j = X M i) else 0) =
    if h : j = i then eqToHom (_ : (embedding C).obj (X M j) = (embedding C).obj (X M i)) else 0
[PROOFSTEP]
ext ⟨⟩ ⟨⟩
[GOAL]
case w.w.H.unit.unit
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j_1 k => if h : j = k then eqToHom (_ : X M j = X M k) else 0) ≫ fun j k =>
        if h : j = i then eqToHom (_ : X M j = X M i) else 0)
      PUnit.unit PUnit.unit =
    dite (j = i) (fun h => eqToHom (_ : (embedding C).obj (X M j) = (embedding C).obj (X M i))) (fun h => 0) PUnit.unit
      PUnit.unit
[PROOFSTEP]
simp only [embedding, comp_apply, comp_dite, dite_comp, comp_zero, zero_comp, Finset.sum_dite_eq', Finset.mem_univ,
  ite_true, eqToHom_refl, Category.comp_id]
[GOAL]
case w.w.H.unit.unit
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (if h : j = i then eqToHom (_ : X M j = X M i) else 0) =
    dite (j = i) (fun h => eqToHom (_ : (embedding C).obj (X M j) = (embedding C).obj (X M i))) (fun h => 0) PUnit.unit
      PUnit.unit
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : j = i
⊢ eqToHom (_ : X M j = X M i) =
    eqToHom (_ : (embedding C).obj (X M j) = (embedding C).obj (X M i)) PUnit.unit PUnit.unit
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
j : M.ι
⊢ eqToHom (_ : X M j = X M j) =
    eqToHom (_ : (embedding C).obj (X M j) = (embedding C).obj (X M j)) PUnit.unit PUnit.unit
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : ¬j = i
⊢ 0 = OfNat.ofNat 0 PUnit.unit PUnit.unit
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ (additiveObjIsoBiproduct F M).hom ≫ biproduct.π (fun i => F.obj ((embedding C).obj (X M i))) i =
    F.map ((isoBiproductEmbedding M).hom ≫ biproduct.π (fun i => (embedding C).obj (X M i)) i)
[PROOFSTEP]
dsimp [additiveObjIsoBiproduct]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ (F.map (biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
        biproduct.lift (Functor.mapBicone F (biproduct.bicone fun i => (embedding C).obj (X M i))).π) ≫
      biproduct.π (fun i => F.obj ((embedding C).obj (X M i))) i =
    F.map
      ((biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
        biproduct.π (fun i => (embedding C).obj (X M i)) i)
[PROOFSTEP]
rw [biproduct.lift_π, Category.assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ F.map (biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
      biproduct.lift (Functor.mapBicone F (biproduct.bicone fun i => (embedding C).obj (X M i))).π ≫
        biproduct.π (fun i => F.obj ((embedding C).obj (X M i))) i =
    F.map fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0
[PROOFSTEP]
erw [biproduct.lift_π, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ F.map
      ((biproduct.lift fun i j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0) ≫
        Bicone.π (biproduct.bicone fun i => (embedding C).obj (X M i)) i) =
    F.map fun j k => if h : j = i then eqToHom (_ : X M j = X M i) else 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ biproduct.ι (fun i => F.obj ((embedding C).obj (X M i))) i ≫ (additiveObjIsoBiproduct F M).inv =
    F.map (biproduct.ι (fun i => (embedding C).obj (X M i)) i ≫ (isoBiproductEmbedding M).inv)
[PROOFSTEP]
dsimp [additiveObjIsoBiproduct, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M : Mat_ C
i : M.ι
⊢ biproduct.ι (fun i => F.obj ((embedding C).obj (X M i))) i ≫
      (biproduct.desc fun j => F.map (biproduct.ι (fun i => (embedding C).obj (X M i)) j)) ≫
        F.map (biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0) =
    F.map
      (biproduct.ι (fun i => (embedding C).obj (X M i)) i ≫
        biproduct.desc fun i j k => if h : i = k then eqToHom (_ : X M i = X M k) else 0)
[PROOFSTEP]
simp only [biproduct.ι_desc, biproduct.ι_desc_assoc, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
⊢ F.map f ≫ (additiveObjIsoBiproduct F N).hom =
    (additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j => F.map ((embedding C).map (f i j))
[PROOFSTEP]
ext i : 1
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
⊢ (F.map f ≫ (additiveObjIsoBiproduct F N).hom) ≫ biproduct.π (fun i => F.obj ((embedding C).obj (X N i))) i =
    ((additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫
      biproduct.π (fun i => F.obj ((embedding C).obj (X N i))) i
[PROOFSTEP]
simp only [Category.assoc, additiveObjIsoBiproduct_hom_π, isoBiproductEmbedding_hom, embedding_obj_ι, embedding_obj_X,
  biproduct.lift_π, biproduct.matrix_π, ← cancel_epi (additiveObjIsoBiproduct F M).inv, Iso.inv_hom_id_assoc]
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
⊢ ((additiveObjIsoBiproduct F M).inv ≫
      F.map f ≫ F.map fun j k => if h : j = i then eqToHom (_ : X N j = X N i) else 0) =
    biproduct.desc fun j => F.map ((embedding C).map (f j i))
[PROOFSTEP]
ext j : 1
[GOAL]
case w.w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ (biproduct.ι (fun i => F.obj ((embedding C).obj (X M i))) j ≫
      (additiveObjIsoBiproduct F M).inv ≫
        F.map f ≫ F.map fun j k => if h : j = i then eqToHom (_ : X N j = X N i) else 0) =
    biproduct.ι (fun i => F.obj ((embedding C).obj (X M i))) j ≫
      biproduct.desc fun j => F.map ((embedding C).map (f j i))
[PROOFSTEP]
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv, biproduct.ι_desc, ← F.map_comp]
[GOAL]
case w.w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ F.map
      ((fun j_1 k => if h : j = k then eqToHom (_ : X M j = X M k) else 0) ≫
        f ≫ fun j k => if h : j = i then eqToHom (_ : X N j = X N i) else 0) =
    F.map ((embedding C).map (f j i))
[PROOFSTEP]
congr 1
[GOAL]
case w.w.e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun j_1 k => if h : j = k then eqToHom (_ : X M j = X M k) else 0) ≫
      f ≫ fun j k => if h : j = i then eqToHom (_ : X N j = X N i) else 0) =
    (embedding C).map (f j i)
[PROOFSTEP]
funext ⟨⟩ ⟨⟩
[GOAL]
case w.w.e_a.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun j_1 k => if h : j = k then eqToHom (_ : X M j = X M k) else 0) ≫
        f ≫ fun j k => if h : j = i then eqToHom (_ : X N j = X N i) else 0)
      PUnit.unit PUnit.unit =
    (embedding C).map (f j i) PUnit.unit PUnit.unit
[PROOFSTEP]
simp [comp_apply, dite_comp, comp_dite]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
⊢ (additiveObjIsoBiproduct F M).inv ≫ F.map f =
    (biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv
[PROOFSTEP]
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
⊢ { obj := fun X => ⨁ fun i => F.obj (CategoryTheory.Mat_.X X i),
          map := fun {X Y} f => biproduct.matrix fun i j => F.map (f i j) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => ⨁ fun i => F.obj (CategoryTheory.Mat_.X X i),
            map := fun {X Y} f => biproduct.matrix fun i j => F.map (f i j) }.obj
        X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
⊢ (biproduct.matrix fun i j => F.map (𝟙 X i j)) = 𝟙 (⨁ fun i => F.obj (CategoryTheory.Mat_.X X i))
[PROOFSTEP]
ext i j
[GOAL]
case w.w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
i j : X.ι
⊢ biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      (biproduct.matrix fun i j => F.map (𝟙 X i j)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i =
    biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      𝟙 (⨁ fun i => F.obj (CategoryTheory.Mat_.X X i)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
i j : X.ι
h : j = i
⊢ biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      (biproduct.matrix fun i j => F.map (𝟙 X i j)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i =
    biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      𝟙 (⨁ fun i => F.obj (CategoryTheory.Mat_.X X i)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
j : X.ι
⊢ biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      (biproduct.matrix fun i j => F.map (𝟙 X i j)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) j =
    biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      𝟙 (⨁ fun i => F.obj (CategoryTheory.Mat_.X X i)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) j
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : Functor.Additive F
X : Mat_ C
i j : X.ι
h : ¬j = i
⊢ biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      (biproduct.matrix fun i j => F.map (𝟙 X i j)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i =
    biproduct.ι (fun i => F.obj (CategoryTheory.Mat_.X X i)) j ≫
      𝟙 (⨁ fun i => F.obj (CategoryTheory.Mat_.X X i)) ≫ biproduct.π (fun i => F.obj (CategoryTheory.Mat_.X X i)) i
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ L.map f ≫
      ((fun M =>
            additiveObjIsoBiproduct L M ≪≫
              (biproduct.mapIso fun i => α.app (X M i)) ≪≫
                (biproduct.mapIso fun i => (embeddingLiftIso F).symm.app (X M i)) ≪≫
                  (additiveObjIsoBiproduct (lift F) M).symm)
          Y✝).hom =
    ((fun M =>
            additiveObjIsoBiproduct L M ≪≫
              (biproduct.mapIso fun i => α.app (X M i)) ≪≫
                (biproduct.mapIso fun i => (embeddingLiftIso F).symm.app (X M i)) ≪≫
                  (additiveObjIsoBiproduct (lift F) M).symm)
          X✝).hom ≫
      (lift F).map f
[PROOFSTEP]
dsimp only [Iso.trans_hom, Iso.symm_hom, biproduct.mapIso_hom]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ L.map f ≫
      (additiveObjIsoBiproduct L Y✝).hom ≫
        (biproduct.map fun b => (α.app (X Y✝ b)).hom) ≫
          (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X Y✝ b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv =
    ((additiveObjIsoBiproduct L X✝).hom ≫
        (biproduct.map fun b => (α.app (X X✝ b)).hom) ≫
          (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X X✝ b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) X✝).inv) ≫
      (lift F).map f
[PROOFSTEP]
simp only [additiveObjIsoBiproduct_naturality_assoc]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun i j => L.map ((embedding C).map (f i j))) ≫
        (biproduct.map fun b => (α.app (X Y✝ b)).hom) ≫
          (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X Y✝ b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv =
    ((additiveObjIsoBiproduct L X✝).hom ≫
        (biproduct.map fun b => (α.app (X X✝ b)).hom) ≫
          (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X X✝ b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) X✝).inv) ≫
      (lift F).map f
[PROOFSTEP]
simp only [biproduct.matrix_map_assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k =>
          L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.map fun b => (α.app (X X✝ b)).hom) ≫
        (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X X✝ b)).hom) ≫
          (additiveObjIsoBiproduct (lift F) X✝).inv ≫ (lift F).map f
[PROOFSTEP]
simp only [additiveObjIsoBiproduct_naturality']
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k =>
          L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.map fun b => (α.app (X X✝ b)).hom) ≫
        (biproduct.map fun b => ((embeddingLiftIso F).symm.app (X X✝ b)).hom) ≫
          (biproduct.matrix fun i j => (lift F).map ((embedding C).map (f i j))) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv
[PROOFSTEP]
simp only [biproduct.map_matrix_assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k =>
          L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k =>
          (α.app (X X✝ j)).hom ≫
            ((embeddingLiftIso F).symm.app (X X✝ j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv
[PROOFSTEP]
congr 3
[GOAL]
case e_a.e_a.e_m
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (fun j k => L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) =
    fun j k =>
    (α.app (X X✝ j)).hom ≫ ((embeddingLiftIso F).symm.app (X X✝ j)).hom ≫ (lift F).map ((embedding C).map (f j k))
[PROOFSTEP]
ext j k
[GOAL]
case e_a.e_a.e_m.h.h
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom =
    (α.app (X X✝ j)).hom ≫ ((embeddingLiftIso F).symm.app (X X✝ j)).hom ≫ (lift F).map ((embedding C).map (f j k))
[PROOFSTEP]
apply biproduct.hom_ext
[GOAL]
case e_a.e_a.e_m.h.h.w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ ∀ (j_1 : ((embedding C).obj (X Y✝ k)).ι),
    (L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) ≫
        biproduct.π (fun i => F.obj (X ((embedding C).obj (X Y✝ k)) i)) j_1 =
      ((α.app (X X✝ j)).hom ≫ ((embeddingLiftIso F).symm.app (X X✝ j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
        biproduct.π (fun i => F.obj (X ((embedding C).obj (X Y✝ k)) i)) j_1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case e_a.e_a.e_m.h.h.w.unit
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ (L.map ((embedding C).map (f j k)) ≫ (α.app (X Y✝ k)).hom ≫ ((embeddingLiftIso F).symm.app (X Y✝ k)).hom) ≫
      biproduct.π (fun i => F.obj (X ((embedding C).obj (X Y✝ k)) i)) PUnit.unit =
    ((α.app (X X✝ j)).hom ≫ ((embeddingLiftIso F).symm.app (X X✝ j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
      biproduct.π (fun i => F.obj (X ((embedding C).obj (X Y✝ k)) i)) PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case e_a.e_a.e_m.h.h.w.unit
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : Functor.Additive F
L : Mat_ C ⥤ D
inst✝ : Functor.Additive L
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ (L.map ((embedding C).map (f j k)) ≫ NatTrans.app α.hom (X Y✝ k) ≫ biproduct.lift fun x => 𝟙 (F.obj (X Y✝ k))) ≫
      biproduct.π (fun i => F.obj (X Y✝ k)) PUnit.unit =
    (NatTrans.app α.hom (X X✝ j) ≫
        (biproduct.lift fun x => 𝟙 (F.obj (X X✝ j))) ≫ biproduct.matrix fun i j_1 => F.map (f j k)) ≫
      biproduct.π (fun i => F.obj (X Y✝ k)) PUnit.unit
[PROOFSTEP]
simpa using α.hom.naturality (f j k)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
R : Type u
⊢ Inhabited (Mat R)
[PROOFSTEP]
dsimp [Mat]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
R : Type u
⊢ Inhabited FintypeCat
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
⊢ ∀ {W X Y Z : Mat R} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
W✝ X✝ Y✝ Z✝ : Mat R
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
simp [Matrix.mul_assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
M : Mat R
i : ↑M
⊢ 𝟙 M i i = 1
[PROOFSTEP]
simp [id_apply]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
M : Mat R
i j : ↑M
h : i ≠ j
⊢ 𝟙 M i j = 0
[PROOFSTEP]
simp [id_apply, h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
⊢ { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (𝟙 X) =
    𝟙 ({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)
⊢ { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (𝟙 X) i✝ j✝ =
    𝟙 ({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X) i✝ j✝
[PROOFSTEP]
simp only [Mat_.id_def, id_def]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)
⊢ MulOpposite.unop (if h : i✝ = j✝ then eqToHom (_ : Mat_.X X i✝ = Mat_.X X j✝) else 0) = if i✝ = j✝ then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)
h✝ : i✝ = j✝
⊢ MulOpposite.unop (eqToHom (_ : Mat_.X X i✝ = Mat_.X X j✝)) = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)
h✝ : ¬i✝ = j✝
⊢ MulOpposite.unop 0 = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (f ≫ g) =
    { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map f ≫
      { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map g
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X✝)
j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj Z✝)
⊢ { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (f ≫ g) i✝ j✝ =
    ({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map f ≫
        { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map g)
      i✝ j✝
[PROOFSTEP]
simp only [Mat_.comp_apply, comp_apply]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X✝)
j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj Z✝)
⊢ MulOpposite.unop (∑ j : Y✝.ι, f i✝ j ≫ g j j✝) =
    ∑ j : ↑(FintypeCat.of Y✝.ι), MulOpposite.unop (f i✝ j) * MulOpposite.unop (g j j✝)
[PROOFSTEP]
apply Finset.unop_sum
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext
[GOAL]
case H
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
i✝ : X✝.ι
j✝ : Y✝.ι
⊢ a₁✝ i✝ j✝ = a₂✝ i✝ j✝
[PROOFSTEP]
apply_fun MulOpposite.unop using MulOpposite.unop_injective
[GOAL]
case H
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
i✝ : X✝.ι
j✝ : Y✝.ι
⊢ MulOpposite.unop (a₁✝ i✝ j✝) = MulOpposite.unop (a₂✝ i✝ j✝)
[PROOFSTEP]
exact congr_fun (congr_fun w _) _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat R
⊢ (equivalenceSingleObjInverse R).obj (Mat_.mk ↑X fun x => PUnit.unit) = X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat R
⊢ FintypeCat.of ↑X = X
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
α✝ : Type
str✝ : Fintype α✝
⊢ FintypeCat.of ↑(Bundled.mk α✝) = Bundled.mk α✝
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X Y : Mat R
⊢ AddCommGroup (X ⟶ Y)
[PROOFSTEP]
change AddCommGroup (Matrix X Y R)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X Y : Mat R
⊢ AddCommGroup (Matrix (↑X) (↑Y) R)
[PROOFSTEP]
infer_instance
