-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem additiveObjIsoBiproduct_naturality (F : Mat_ C ⥤ D) [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))

Proof state:
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✝ : F.Additive
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))

Tactic:
ext i : 1

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

Proof state:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ F.map ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) =
    F.map ((embedding C).map (f j i))

Tactic:
congr 1

Result:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) =
    (embedding C).map (f j i)

Proof state:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) =
    (embedding C).map (f j i)

Tactic:
funext ⟨⟩ ⟨⟩

Result:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) PUnit.unit
      PUnit.unit =
    (embedding C).map (f j i) PUnit.unit PUnit.unit

Proof state:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) PUnit.unit
      PUnit.unit =
    (embedding C).map (f j i) PUnit.unit PUnit.unit

Tactic:
simp [comp_apply, dite_comp, comp_dite]

Result:
no goals

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

Tactic:
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]

Result:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
⊢ ((additiveObjIsoBiproduct F M).inv ≫ F.map f ≫ F.map fun j x => if h : j = i then eqToHom ⋯ else 0) =
    biproduct.desc fun j => F.map ((embedding C).map (f j i))

Proof state:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
⊢ ((additiveObjIsoBiproduct F M).inv ≫ F.map f ≫ F.map fun j x => if h : j = i then eqToHom ⋯ else 0) =
    biproduct.desc fun j => F.map ((embedding C).map (f j i))

Tactic:
ext j : 1

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

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

Tactic:
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
  biproduct.ι_desc, ← F.map_comp]

Result:
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✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ F.map ((fun x k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x => if h : j = i then eqToHom ⋯ else 0) =
    F.map ((embedding C).map (f j 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
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
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))

Tactic:
classical
ext i : 1
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]
ext j : 1
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
  biproduct.ι_desc, ← F.map_comp]
congr 1
funext ⟨⟩ ⟨⟩
simp [comp_apply, dite_comp, comp_dite]

Result:
no goals