C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
refine' biproduct.hom_ext _ _ (fun i => _)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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
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]
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
refine' biproduct.hom_ext' _ _ (fun j => _)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
  biproduct.ι_desc, ← F.map_comp]
case e_a
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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))
congr 1
case e_a.h.h
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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
case e_a
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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)
funext ⟨⟩ ⟨⟩
no goals
case e_a.h.h
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category 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
simp [comp_apply, dite_comp, comp_dite]