-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : (↑s.1 : Type (max v w))
simp :
  (fun (j : J) ↦
      HAdd.hAdd (α := (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w))) (β :=
        (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
                (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
                (s.π.app { as := j }) :
              (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
            x :
          (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
                (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
                (s.π.app { as := j }) :
              (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
            y :
          (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))) =
    HAdd.hAdd (α := (j : J) → (↑(f j) : Type (max v w)))
      (fun (j : J) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
              (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
              (s.π.app { as := j : Discrete J }) :
            (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
          x)
      fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
            (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
            (s.π.app { as := j : Discrete J }) :
          (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
        y
⊢ (fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
            (CC := carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j }) :
          (a : (↑(((Functor.const (Discrete J)).obj s.pt).obj { as := j }) : Type (max v w))) →
            (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
        (x + y)) =
    HAdd.hAdd (α := (j : J) → (↑(f j) : Type (max v w)))
      (fun (j : J) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
              (CC := carrier) (X :=
              Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
              (s.π.app { as := j : Discrete J }) :
            (a : (↑(((Functor.const (Discrete J)).obj s.pt).obj { as := j }) : Type (max v w))) →
              (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
          x)
      fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
            (CC := carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j : Discrete J }) :
          (a : (↑(((Functor.const (Discrete J)).obj s.pt).obj { as := j }) : Type (max v w))) →
            (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
        y

Tactic:
simp only [Functor.const_obj_obj, map_add]

Premises used: map_add, CategoryTheory.Functor.const_obj_obj