awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
j : J
x :
  ((F ⋙
          forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier)
            MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j
⊢ HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v)))
      (G.mk F
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                      (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x))⁻¹
      (G.mk F
        (Sigma.mk (β := fun (j : J) ↦
          ((F ⋙
                  forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CD := MonCat.carrier)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).obj
            j)
          j x)) =
    1

Tactic:
simp [colimit_inv_mk_eq, colimit_mul_mk_eq F ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
        colimit_one_eq F j]

Premises used: GrpCat.FilteredColimits.colimit_inv_mk_eq, CategoryTheory.CategoryStruct.id, GrpCat.FilteredColimits.colimit_mul_mk_eq, Sigma.mk, GrpCat.FilteredColimits.colimit_one_eq
-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
⊢ PreservesFilteredColimits
    (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ GrpCat MonCat) (forget MonCat.{u})

Premises used: GrpCat, CategoryTheory.Functor.comp, MonCat, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommGrpCat
⊢ PreservesFilteredColimits
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ CommGrpCat GrpCat) (forget GrpCat.{u})

Premises used: GrpCat, CategoryTheory.Functor.comp, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CommGrpCat, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Grp.FiniteGrp
Goal:
G : FiniteGrp.{u_1}
⊢ Finite.{u_1 + 1} (↑G.toGrp : Type u_1)

Tactic:
G.isFinite

Premises used: FiniteGrp.isFinite
-- Module: Mathlib.Algebra.Category.Grp.FiniteGrp
Goal:
X Y : Type u
inst : Group X
inst_1 : Finite X
inst_2 : Group Y
inst_3 : Finite Y
f : X →* Y
x : X
⊢ Eq (α := (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (of Y))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := of X) (Y := of Y) (ofHom f) :
          (a : (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (of X)) →
            (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (of Y))
        x :
      (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (of Y))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' GrpCat.coyonedaObjIsoForget

Premises used: CategoryTheory.Functor.IsCorepresentable.mk', GrpCat.coyonedaObjIsoForget
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' CommGrpCat.coyonedaObjIsoForget

Premises used: CommGrpCat.coyonedaObjIsoForget, CategoryTheory.Functor.IsCorepresentable.mk'
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget AddGrpCat (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' AddGrpCat.coyonedaObjIsoForget

Premises used: AddGrpCat.coyonedaObjIsoForget, CategoryTheory.Functor.IsCorepresentable.mk'
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' AddCommGrpCat.coyonedaObjIsoForget

Premises used: AddCommGrpCat.coyonedaObjIsoForget, CategoryTheory.Functor.IsCorepresentable.mk'
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
G : Type u
inst : AddCommGroup G
x y : G
h :
  ∀ (x_1 : ULift.{u, 0} ℤ),
    Eq (α := G)
      ((((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) (x + y) : ULift.{u, 0} ℤ →+ G) :
            (a : ULift.{u, 0} ℤ) → G)
          x_1 :
        G)
      ((HAdd.hAdd (α := ULift.{u, 0} ℤ →+ G) (β := ULift.{u, 0} ℤ →+ G)
              ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) x : ULift.{u, 0} ℤ →+ G)
              ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) y : ULift.{u, 0} ℤ →+ G) :
            (a : ULift.{u, 0} ℤ) → G)
          x_1 :
        G)
⊢ (uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) (x + y) =
    HAdd.hAdd (α := ULift.{u, 0} ℤ →+ G) (β := ULift.{u, 0} ℤ →+ G)
      ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) x : ULift.{u, 0} ℤ →+ G)
      ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) y : ULift.{u, 0} ℤ →+ G)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Goal:
G : Type u
inst : AddCommGroup G
x y : G
x_1 : ULift.{u, 0} ℤ
⊢ Eq (α := G)
    ((((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) (x + y) : ULift.{u, 0} ℤ →+ G) : (a : ULift.{u, 0} ℤ) → G)
        x_1 :
      G)
    ((HAdd.hAdd (α := ULift.{u, 0} ℤ →+ G) (β := ULift.{u, 0} ℤ →+ G)
            ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) x : ULift.{u, 0} ℤ →+ G)
            ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) y : ULift.{u, 0} ℤ →+ G) :
          (a : ULift.{u, 0} ℤ) → G)
        x_1 :
      G)

Tactic:
simp_all only [uliftZMultiplesHom_apply_apply, smul_add, AddMonoidHom.add_apply]

Premises used: uliftZMultiplesHom_apply_apply, AddMonoidHom.add_apply, smul_add
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
⊢ Mono (image.ι f)

Tactic:
ConcreteCategory.mono_of_injective (image.ι f) Subtype.val_injective

Premises used: Subtype.val_injective, CategoryTheory.ConcreteCategory.mono_of_injective, AddCommGrpCat.image.ι
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
hf :
  ∀ (x : (↑G : Type)),
    Eq (α := (↑H : Type)) ((Hom.hom (factorThruImage f ≫ ι f) : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
      ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
⊢ factorThruImage f ≫ ι f = f

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑G : Type)
⊢ Eq (α := (↑H : Type)) ((Hom.hom (factorThruImage f ≫ ι f) : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
    ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ Mono F'.m

Tactic:
haveI := F'.m_mono
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
a :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                F'.e :
              (a : (↑G : Type)) → (↑F'.I : Type))
            (↑(Classical.indefiniteDescription
                  (fun (x : (↑G : Type)) ↦
                    Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                      ((↑0 : (↑H : Type)) : (↑H : Type)))
                  ⋯) :
              (↑G : Type)) :
          (↑F'.I : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))
⊢ Eq (α := (↑F'.1 : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.e :
          (a : (↑G : Type)) → (↑F'.I : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑F'.I : Type))
    (0 : (↑F'.1 : Type))

Tactic:
apply injective_of_mono F'.m

Premises used: AddCommGrpCat.injective_of_mono, CategoryTheory.Limits.MonoFactorisation.m
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
a :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                F'.e :
              (a : (↑G : Type)) → (↑F'.I : Type))
            (↑(Classical.indefiniteDescription
                  (fun (x : (↑G : Type)) ↦
                    Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                      ((↑0 : (↑H : Type)) : (↑H : Type)))
                  ⋯) :
              (↑G : Type)) :
          (↑F'.I : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))

Tactic:
change (F'.e ≫ F'.m) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
a :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    (0 : (↑H : Type))
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))

Tactic:
rw [F'.fac, map_zero]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, map_zero
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    (0 : (↑H : Type))

Tactic:
(Classical.indefiniteDescription (fun y => f y = 0) _).2

Premises used: Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, OfNat.ofNat, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    (0 : (↑H : Type))

Tactic:
exact (Classical.indefiniteDescription (fun y => f y = 0) _).2

Premises used: Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, OfNat.ofNat, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Mono F'.m

Tactic:
haveI := F'.m_mono
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
a :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))

Tactic:
rw [F'.fac]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
a :
  (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))

Tactic:
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]

Premises used: Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
a :
  (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (β := (↑H : Type)) (↑x : (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
⊢ (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))

Tactic:
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]

Premises used: Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
a : (↑(x + y) : (↑H : Type)) = (↑x : (↑H : Type)) + (↑y : (↑H : Type))
⊢ (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (β := (↑H : Type)) (↑x : (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))

Tactic:
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]

Premises used: Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (↑(x + y) : (↑H : Type)) = (↑x : (↑H : Type)) + (↑y : (↑H : Type))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
hf :
  ∀ (x : (↑(image f) : Type)),
    Eq (α := (↑H : Type)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
      ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type)
hf :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
⊢ Eq (α := (↑H : Type)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))

Tactic:
change (F'.e ≫ F'.m) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe