awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type w
f : J → AddCommGrpCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor f)
      { pt := of ((j : J) → (↑(f j) : Type (max u w))),
        π :=
          Discrete.natTrans fun (j : Discrete J) ↦
            ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := of ((j : J) → (↑(f j) : Type (max u w))),
              π :=
                Discrete.natTrans fun (j : Discrete J) ↦
                  ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) })
          j =
      s.π.app j
x : (↑s.pt : Type (max u w))
j : J
⊢ Eq (α := (↑(f j) : Type (max u w)))
    ((Hom.hom m :
          (a : (↑s.pt : Type (max u w))) →
            (↑{ pt := of ((j : J) → (↑(f j) : Type (max u w))),
                    π :=
                      Discrete.natTrans fun (j : Discrete J) ↦
                        ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }.pt :
              Type (max u w)))
        x j :
      (↑(f j) : Type (max u w)))
    ((Hom.hom (lift.{w, u} f s) :
          (a : (↑s.pt : Type (max u w))) →
            (↑{ pt := of ((j : J) → (↑(f j) : Type (max u w))),
                    π :=
                      Discrete.natTrans fun (j : Discrete J) ↦
                        ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }.pt :
              Type (max u w)))
        x j :
      (↑(f j) : Type (max u w)))

Tactic:
CategoryTheory.congr_fun (w ⟨j⟩) x

Premises used: CategoryTheory.congr_fun, CategoryTheory.Discrete.mk
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type w
f : J → AddCommGrpCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor f)
      { pt := of ((j : J) → (↑(f j) : Type (max u w))),
        π :=
          Discrete.natTrans fun (j : Discrete J) ↦
            ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := of ((j : J) → (↑(f j) : Type (max u w))),
              π :=
                Discrete.natTrans fun (j : Discrete J) ↦
                  ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) })
          j =
      s.π.app j
x : (↑s.pt : Type (max u w))
j : J
⊢ Eq (α := (↑(f j) : Type (max u w)))
    ((Hom.hom m :
          (a : (↑s.pt : Type (max u w))) →
            (↑{ pt := of ((j : J) → (↑(f j) : Type (max u w))),
                    π :=
                      Discrete.natTrans fun (j : Discrete J) ↦
                        ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }.pt :
              Type (max u w)))
        x j :
      (↑(f j) : Type (max u w)))
    ((Hom.hom (lift.{w, u} f s) :
          (a : (↑s.pt : Type (max u w))) →
            (↑{ pt := of ((j : J) → (↑(f j) : Type (max u w))),
                    π :=
                      Discrete.natTrans fun (j : Discrete J) ↦
                        ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type (max u w))) j.as) }.pt :
              Type (max u w)))
        x j :
      (↑(f j) : Type (max u w)))

Tactic:
exact CategoryTheory.congr_fun (w ⟨j⟩) x

Premises used: CategoryTheory.congr_fun, CategoryTheory.Discrete.mk
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type
inst : Finite J
f : J → AddCommGrpCat
j : J
⊢ CategoryStruct.comp (Y := ⨁ f) (Iso.inv (biproductIsoPi f) : of ((j : J) → (↑(f j) : Type u)) ⟶ ⨁ f)
      (biproduct.π f j : ⨁ f ⟶ f j) =
    ofHom (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(f j) : Type u)) j)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk j)

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
⊢ tensorObj (𝒞 := instCategory) G H = of ((↑G : Type u) × (↑H : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
p : (↑G : Type u)
q : (↑H : Type u)
fst :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1
snd :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2
⊢ (hom (FC := TypeCat.Fun)
          (Functor.LaxMonoidal.μ
            (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
        (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
          (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
      (p, q) =
    (p, q)

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget GrpCat.{u}) G H) (p, q)

Premises used: GrpCat, Prod.mk, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget GrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget GrpCat.{u}) G H) (p, q)

Premises used: GrpCat, Prod.mk, CategoryTheory.forget, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : GrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) G H) :
          (a : (fun (X : Type u) ↦ X) ((forget GrpCat).obj G ⊗ (forget GrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget GrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget GrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
⊢ tensorObj (𝒞 := instCategory) G H = of ((↑G : Type u) × (↑H : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
fst :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1
snd :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2
⊢ (hom (FC := TypeCat.Fun)
          (Functor.LaxMonoidal.μ
            (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)) G
            H) :
        (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
          (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
      (p, q) =
    (p, q)

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, AddGrpCat, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, AddGrpCat, CategoryTheory.forget, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj G ⊗ (forget AddGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
⊢ tensorObj (𝒞 := instCategory) G H = of ((↑G : Type u) × (↑H : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
fst :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1
snd :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2
⊢ (hom (FC := TypeCat.Fun)
          (Functor.LaxMonoidal.μ
            (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
            G H) :
        (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
          (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
      (p, q) =
    (p, q)

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget CommGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, CategoryTheory.Functor.Monoidal.μ_fst, CommGrpCat, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget CommGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, CommGrpCat, CategoryTheory.forget, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : CommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj G ⊗ (forget CommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget CommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
⊢ tensorObj (𝒞 := instCategory) G H = of ((↑G : Type u) × (↑H : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
fst :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1
snd :
  ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2
⊢ (hom (FC := TypeCat.Fun)
          (Functor.LaxMonoidal.μ
            (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier))
            G H) :
        (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
          (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
      (p, q) =
    (p, q)

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddCommGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, CategoryTheory.Functor.Monoidal.μ_fst, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).1 =
    (p, q).1

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddCommGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddCommGrpCat.{u}) G H) (p, q)

Premises used: Prod.mk, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Goal:
G H : AddCommGrpCat
p : (↑G : Type u)
q : (↑H : Type u)
⊢ ((hom (FC := TypeCat.Fun)
            (Functor.LaxMonoidal.μ
              (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier))
              G H) :
          (a : (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj G ⊗ (forget AddCommGrpCat).obj H)) →
            (fun (X : Type u) ↦ X) ((forget AddCommGrpCat).obj (G ⊗ H)))
        (p, q)).2 =
    (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddCommGrpCat.{u}) G H) (p, q)
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
α : Type u_1
inst_2 : AddMonoid α
f g : Quot F →+ α
h :
  ∀ (j : J) (x : (↑(F.obj j) : Type w)),
    Eq.{u_1 + 1} (α := α) ((f : (a : Quot F) → α) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x : Quot F) : α)
      ((g : (a : Quot F) → α) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x : Quot F) : α)
⊢ f = g

Tactic:
QuotientAddGroup.addMonoidHom_ext _ (DFinsupp.addHom_ext h)

Premises used: QuotientAddGroup.addMonoidHom_ext, AddCommGrpCat.Colimits.Quot, DFinsupp.addHom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
refine :
  Relations F ≤
    AddMonoidHom.ker (M := (↑c.pt : Type w))
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))
⊢ Quot F →+ (↑c.pt : Type w)

Tactic:
refine QuotientAddGroup.lift _ (DFinsupp.sumAddHom fun x => (c.ι.app x).hom) ?_

Premises used: QuotientAddGroup.lift
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
dsimp :
  Relations F ≤
    AddMonoidHom.ker (M := (↑c.pt : Type w))
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))
⊢ Relations F ≤
    AddMonoidHom.ker (M := (↑c.pt : Type w))
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
rw :
  {x : Π₀ (j : J), (↑(F.obj j) : Type w) |
      ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑(F.obj j) : Type w)),
        x =
          HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    carrier) (F.map u) :
                  (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
                a))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a)} ⊆
    (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
⊢ Relations F ≤
    AddMonoidHom.ker (M := (↑c.pt : Type w))
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))

Tactic:
rw [AddSubgroup.closure_le]

Premises used: AddSubgroup.closure_le