-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this_2 : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ Eq.{v + 1} (α :=
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
    (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
have rw : Eq (α :=
  tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
      (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
  (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd) :
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
  ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier))
          (tensorObj (𝒞 := instCategory) (F.obj X) (F.obj X)))
        (Functor.LaxMonoidal.μ
          (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier))
          (F.obj X) (F.obj X))
        (CategoryTheory.Functor.map
          (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier))
          (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X) +
            SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X))) :
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
Tactic: rw [Functor.obj.μ_def X (F := F ⋙ forget AddCommGrpCat), Preadditive.mul_def X,
    Functor.comp_map, F.map_add,
    Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X,
    Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
    Functor.Monoidal.μ_snd]