-- Mathlib/CategoryTheory/Preadditive/Mat.lean
@[reassoc (attr := simp)]
lemma additiveObjIsoBiproduct_hom_π (F : Mat_ C ⥤ D) [Functor.Additive F] (M : Mat_ C) (i : M.ι) :
    (additiveObjIsoBiproduct F M).hom ≫ biproduct.π _ i =
      F.map (M.isoBiproductEmbedding.hom ≫ biproduct.π _ i)

Proof state:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map
      ((biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        (biproduct.bicone fun i => (embedding C).obj (M.X i)).π i) =
    F.map fun j x => if h : j = i then eqToHom ⋯ else 0

Tactic:
simp

Result:
no goals

Proof state:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ (F.map (biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π) ≫
      biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i =
    F.map
      ((biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.π (fun i => (embedding C).obj (M.X i)) i)

Tactic:
rw [biproduct.lift_π, Category.assoc]

Result:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map (biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
      biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π ≫
        biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i =
    F.map fun j x => if h : j = i then eqToHom ⋯ else 0

Proof state:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map (biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
      biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π ≫
        biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i =
    F.map fun j x => if h : j = i then eqToHom ⋯ else 0

Tactic:
erw [biproduct.lift_π, ← F.map_comp]

Result:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map
      ((biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        (biproduct.bicone fun i => (embedding C).obj (M.X i)).π i) =
    F.map fun j x => if h : j = i then eqToHom ⋯ else 0

Proof state:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ (additiveObjIsoBiproduct F M).hom ≫ biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i =
    F.map (M.isoBiproductEmbedding.hom ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i)

Tactic:
dsimp [additiveObjIsoBiproduct]

Result:
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✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ (F.map (biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π) ≫
      biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i =
    F.map
      ((biproduct.lift fun i j x => if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.π (fun i => (embedding C).obj (M.X i)) i)