-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Biproducts (goal)
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))
⊢ (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
have 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
Tactic: simp only [Functor.const_obj_obj, map_add]