awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Biproducts (goal)
Goal:
J : Type w
f : J → AddCommGrpCat
s : Fan f
⊢ Eq (α := (j : J) → (↑(f j) : Type (max u w)))
    (fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u w)) →+ (↑x2 : Type (max u 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 u w))) →
            (↑((Discrete.functor f).obj { as := j }) : Type (max u w)))
        0)
    0
have simp : Eq (α := (j : J) → (↑(f j) : Type (max u w))) (fun (j : J) ↦ 0) 0
Tactic: simp only [Functor.const_obj_obj, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Biproducts (goal)
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
⊢ m = lift.{w, u} f s
have hf : ∀ (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: ext x j
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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) =
    (p, q)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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
⊢ (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)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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) =
    (p, q)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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
⊢ (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)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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) =
    (p, q)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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
⊢ (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)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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) =
    (p, q)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.CartesianMonoidal (goal)
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
⊢ (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)
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
⊢ Quot F →+ (↑c.pt : Type w)
have 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))
Tactic: refine QuotientAddGroup.lift _ (DFinsupp.sumAddHom fun x => (c.ι.app x).hom) ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
⊢ 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))
have 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)))
Tactic: rw [AddSubgroup.closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
⊢ Membership.mem (γ := Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
      {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)}
      a →
    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)))
have this : ∀ (w w_1 : J) (w_2 : w ⟶ w_1) (w_3 : (↑(F.obj w) : Type w))
  (eq :
    a =
      HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
        (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map w_2) :
              (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
            w_3))
        (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)),
  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)))
Tactic: ⟨_, _, _, _, eq⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
⊢ 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)))
have rw : HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
    (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (F.map w_2) :
          (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
        w_3))
    (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3) ∈
  (↑(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)))
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
⊢ HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3) ∈
    (↑(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)))
have simp : HSub.hSub (α := (↑c.pt : Type w)) (β := (↑c.pt : Type w))
    ((Hom.hom (c.ι.app w_1) : (a : (↑(F.obj w_1) : Type w)) → (↑c.pt : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map w_2) :
              (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
            w_3 :
          (↑(F.obj w_1) : Type w)) :
      (↑c.pt : Type w))
    ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
  0
Tactic: simp only [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
⊢ HSub.hSub (α := (↑c.pt : Type w)) (β := (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w_1) : (a : (↑(F.obj w_1) : Type w)) → (↑c.pt : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  carrier) (F.map w_2) :
                (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
              w_3 :
            (↑(F.obj w_1) : Type w)) :
        (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0
have change : HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (F.map w_2 ≫ c.ι.app w_1) :
          (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
        w_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
    ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
  0
Tactic: change (F.map _ ≫ c.ι.app _) _ - _ = 0
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
⊢ HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (F.map w_2 ≫ c.ι.app w_1) :
            (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
          w_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0
have rw : HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (c.ι.app w ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) c.pt) w_2) :
          (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
        w_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
    ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
  0
Tactic: rw [c.ι.naturality]