awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑(toCocone F f).pt : Type w))
    ((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : (a : Quot F) → (↑(toCocone F f).pt : Type w))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))
have rw : Eq (α := (↑(toCocone F f).pt : Type w))
  ((Hom.hom (hc.desc (toCocone F f)) : (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (c.ι.app j) :
            (a : (↑(F.obj j) : Type w)) → (↑(((Functor.const J).obj c.pt).obj j) : Type w))
          x :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j) : Type w)) :
    (↑(toCocone F f).pt : Type w))
  ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
    (↑(toCocone F f).pt : Type w))
Tactic: rw [AddMonoidHom.comp_apply, ι_desc]
-- 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 : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((Hom.hom (hc.desc (toCocone F f)) : (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (c.ι.app j) :
              (a : (↑(F.obj j) : Type w)) → (↑(((Functor.const J).obj c.pt).obj j) : Type w))
            x :
          (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j) : Type w)) :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))
have change : Eq (α := (↑(toCocone F f).pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
          (Y := (toCocone F f).pt) (c.ι.app j ≫ hc.desc (toCocone F f)) :
        (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
      x :
    (↑(toCocone F f).pt : Type w))
  ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
    (↑(toCocone F f).pt : Type w))
Tactic: change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _
-- 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 : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (c.ι.app j ≫ hc.desc (toCocone F f)) :
          (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
        x :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))
have rw : Eq (α := (↑(toCocone F f).pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
          ((toCocone F f).ι.app j) :
        (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
      x :
    (↑(toCocone F f).pt : Type w))
  ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
    (↑(toCocone F f).pt : Type w))
Tactic: rw [hc.fac]
-- 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 : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
| ((f : (a : Quot F) → A) x : A)
have rw : (((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : Quot F →+ (↑(toCocone F f).pt : Type w)) :
      (a : Quot F) → A)
    x :
  A)
Tactic: rw [← Quot.desc_toCocone_desc F c f hc]
-- 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 : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (hc.desc (toCocone F f)) :
          (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
        ((desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → A) x : A)
have conv_rhs : Eq (α := (↑(toCocone F f).pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
          (Y := (toCocone F f).pt) (hc.desc (toCocone F f)) :
        (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
      ((desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
    (↑(toCocone F f).pt : Type w))
  (((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : Quot F →+ (↑(toCocone F f).pt : Type w)) :
        (a : Quot F) → A)
      x :
    A)
Tactic: conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
⊢ c.ι.app j ≫
      ofHom
        (AddMonoidHom.comp (Quot.desc F s)
          (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h)))) =
    s.ι.app j
have hf : ∀ (x : (↑(F.obj j) : Type w)),
  Eq (α := (↑s.pt : Type w))
    ((Hom.hom
            (c.ι.app j ≫
              ofHom
                (AddMonoidHom.comp (Quot.desc F s)
                  (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
Tactic: ext x
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom
            (c.ι.app j ≫
              ofHom
                (AddMonoidHom.comp (Quot.desc F s)
                  (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
have hf : Eq.{w + 1} (α := (↑s.pt : Type w))
  ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
      ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
        ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
    (↑s.pt : Type w))
  ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
Tactic: dsimp
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
| ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
      ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
        ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
    (↑s.pt : Type w))
have erw : ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
    ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
      ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
  (↑s.pt : Type w))
Tactic: erw [← Quot.ι_desc F c j x]
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
have hf : Eq.{w + 1} (α := (↑s.pt : Type w))
  ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
      ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
    (↑s.pt : Type w))
  ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
Tactic: conv_lhs => erw [← Quot.ι_desc F c j x]
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
have hf : Eq.{w + 1} (α := (↑s.pt : Type w))
  ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
    (↑s.pt : Type w))
  ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
Tactic: rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    ofHom
      (AddMonoidHom.comp (Quot.desc F s)
        (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))
have hf : ∀ (x : (↑c.pt : Type w)),
  Eq (α := (↑s.pt : Type w)) ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
    ((Hom.hom
            (ofHom
              (AddMonoidHom.comp (Quot.desc F s)
                (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
Tactic: ext x
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : (↑c.pt : Type w)
⊢ Eq (α := (↑s.pt : Type w)) ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
    ((Hom.hom
            (ofHom
              (AddMonoidHom.comp (Quot.desc F s)
                (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
have hf : ∀ (x : Quot F),
  Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Hom.hom
            (ofHom
              (AddMonoidHom.comp (Quot.desc F s)
                (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
Tactic: obtain ⟨x, rfl⟩ := h.2 x
Cleared hypotheses: x
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x)) :
      (↑s.pt : Type w))
have hf : Eq (α := (↑s.pt : Type w))
  ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
      ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
    (↑s.pt : Type w))
  ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
Tactic: rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]
-- 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
have rw : Eq (α := (↑s.pt : Type w))
  ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
      ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
    (↑s.pt : Type w))
  (((Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) :
        (a : Quot F) → (↑s.pt : Type w))
      x :
    (↑s.pt : 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
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
have hf : (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s
Tactic: suffices eq : m.hom.comp (AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s by
      rw [← eq]; rfl
-- 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
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
⊢ Eq (α :=
    F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)
    (F.map x_2 ≫
        ofHom
          (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) (Quot.ι F x_1)) :
      F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)
    (ofHom (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) (Quot.ι F x)) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2 :
      F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)
have hf : ∀ (x_3 : (↑(F.obj x) : Type w)),
  Eq (α :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) : Type w))
    ((Hom.hom
            (F.map x_2 ≫
              ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x_1))) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
    ((Hom.hom
            (ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
Tactic: 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
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
x_3 : (↑(F.obj x) : Type w)
⊢ Eq (α :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) : Type w))
    ((Hom.hom
            (F.map x_2 ≫
              ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x_1))) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
    ((Hom.hom
            (ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
have hf : Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
  ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
      ((Quot.ι F x_1 : (a : (↑(F.obj x_1) : Type w)) → Quot F)
          ((Hom.hom (F.map x_2) : (a : (↑(F.obj x) : Type w)) → (↑(F.obj x_1) : Type w)) x_3) :
        Quot F) :
    Shrink.{w, max u w} (Quot F))
  ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
      ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
    Shrink.{w, max u w} (Quot F))
Tactic: dsimp
-- 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
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
x_3 : (↑(F.obj x) : Type w)
⊢ Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x_1 : (a : (↑(F.obj x_1) : Type w)) → Quot F)
            ((Hom.hom (F.map x_2) : (a : (↑(F.obj x) : Type w)) → (↑(F.obj x_1) : Type w)) x_3) :
          Quot F) :
      Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
      Shrink.{w, max u w} (Quot F))
have hf : Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
  ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
      ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
    Shrink.{w, max u w} (Quot F))
  ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
      ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
    Shrink.{w, max u w} (Quot F))
Tactic: rw [Quot.map_ι]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : DecidableEq J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_2 : Small.{w, max u w} (Quot F)
⊢ Eq (α := Quot F →+ (↑(colimitCocone F).pt : Type w)) (desc F (colimitCocone F))
    (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
have refine : ∀ (j : J) (x : (↑(F.obj j) : Type w)),
  Eq.{w + 1} (α := (↑(colimitCocone F).pt : Type w))
    ((desc F (colimitCocone F) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(colimitCocone F).pt : Type w))
    ((AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(colimitCocone F).pt : Type w))
Tactic: refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)