-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
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
h :
  ∀
    (x :
      tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))) x =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((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)))))
        x
⊢ 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:
ext