-- 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
x :
  tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ (Multiplicative.toAdd :
        (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) μ :
            (a :
                (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ×
                  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) →
              (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X)
          x :
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) =
    HAdd.hAdd (α := (↑(F.obj X) : Type v)) (β := (↑(F.obj X) : Type v))
      ((Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)) :
            (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (Functor.LaxMonoidal.μ
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                        (CC := carrier))
                      (F.obj X) (F.obj X)) :
                  TypeCat.Fun
                    (ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                        (F.obj X) ×
                      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                        (F.obj X))
                    (ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                      (tensorObj (𝒞 := instCategory) (F.obj X) (F.obj X)))) :
                (a : ToType (F.obj X) × ToType (F.obj X)) → ToType (F.obj X ⊗ F.obj X))
              (((Multiplicative.toAdd :
                      (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                    x.1,
                  (Multiplicative.toAdd :
                      (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                    x.2) :
                ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                    (F.obj X) ×
                  ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                    (F.obj X)) :
            ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
              (tensorObj (𝒞 := instCategory) (F.obj X) (F.obj X))) :
        (↑(F.obj X) : Type v))
      ((Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)) :
            (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (Functor.LaxMonoidal.μ
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                        (CC := carrier))
                      (F.obj X) (F.obj X)) :
                  TypeCat.Fun
                    (ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                        (F.obj X) ×
                      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                        (F.obj X))
                    (ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                      (tensorObj (𝒞 := instCategory) (F.obj X) (F.obj X)))) :
                (a : ToType (F.obj X) × ToType (F.obj X)) → ToType (F.obj X ⊗ F.obj X))
              (((Multiplicative.toAdd :
                      (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                    x.1,
                  (Multiplicative.toAdd :
                      (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                    x.2) :
                ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                    (F.obj X) ×
                  ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
                    (F.obj X)) :
            ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier)
              (tensorObj (𝒞 := instCategory) (F.obj X) (F.obj X))) :
        (↑(F.obj X) : Type v))
have h : (Multiplicative.toAdd :
      (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) μ :
          (a :
              (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ×
                (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) →
            (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X)
        x :
      (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) =
  HAdd.hAdd (α := (↑(F.obj X) : Type v)) (β := (↑(F.obj X) : Type v))
    ((Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)) :
          (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
        (((Multiplicative.toAdd :
                (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
              x.1,
            (Multiplicative.toAdd :
                (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
              x.2) :
          (↑(F.obj X) : Type v) × (↑(F.obj X) : Type v)) :
      (↑(F.obj X) : Type v))
    ((Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)) :
          (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
        (((Multiplicative.toAdd :
                (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
              x.1,
            (Multiplicative.toAdd :
                (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
              x.2) :
          (↑(F.obj X) : Type v) × (↑(F.obj X) : Type v)) :
      (↑(F.obj X) : Type v))
Tactic: rw [dsimp% [types_tensorObj_def, types_tensorUnit_def] μ_forget_apply]