awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G H : CommGrpCat
g : (↑G : Type u_1)
⊢ Eq (α := (↑H : Type u_1))
    ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1))
            carrier _ _ G H 1 :
          (a : (↑G : Type u_1)) → (↑H : Type u_1))
        g :
      (↑H : Type u_1))
    (1 : (↑H : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
a₁ : X →* Y
_ :
  ∀ ⦃a₂ : X →* Y⦄,
    Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂) → a₁ = a₂
⊢ ∀ ⦃a₂ : X →* Y⦄,
    Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂) → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
a₁ a₂ : X →* Y
h : Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂)
h₁ : ∀ (x : X), Eq (α := Y) ((a₁ : (a : X) → Y) x : Y) ((a₂ : (a : X) → Y) x : Y)
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
a₁ a₂ : X →* Y
h : Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂)
x : X
⊢ Eq (α := Y) ((a₁ : (a : X) → Y) x : Y) ((a₂ : (a : X) → Y) x : Y)

Tactic:
apply ConcreteCategory.congr_hom h

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R S : CommGrpCat
i : R ⟶ S
r : (↑R : Type u_1)
h : r = 1
⊢ Eq (α := (↑S : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            i :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        r :
      (↑S : Type u_1))
    (1 : (↑S : Type u_1))

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : CommGrpCat
⊢ ofHom
      (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
        ((Hom.hom (𝟙 X)).comp (MulEquiv.toMonoidHom MulEquiv.ulift))) =
    𝟙 (of (ULift.{u, v} (↑X : Type v)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : CommGrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := of (ULift.{u, v} (↑X : Type v)) ⟶ of (ULift.{u, v} (↑Z : Type v)))
    (ofHom
      (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
        ((Hom.hom (f ≫ g)).comp (MulEquiv.toMonoidHom MulEquiv.ulift))))
    (CategoryStruct.comp (Y := of (ULift.{u, v} (↑Y : Type v)))
      (ofHom
        (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
          ((Hom.hom f).comp (MulEquiv.toMonoidHom MulEquiv.ulift))))
      (ofHom
        (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
          ((Hom.hom g).comp (MulEquiv.toMonoidHom MulEquiv.ulift)))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G : AddCommGrpCat
h k : (↑G : Type)
w : asHom h = asHom k
⊢ h = k

Tactic:
simpa using CategoryTheory.congr_fun w 1

Premises used: CategoryTheory.congr_fun, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G : AddCommGrpCat
f g : of ℤ ⟶ G
w :
  Eq (α := (↑G : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑(of ℤ) : Type)) → (↑G : Type))
        1 :
      (↑G : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) g :
          (a : (↑(of ℤ) : Type)) → (↑G : Type))
        1 :
      (↑G : Type))
⊢ f = g

Tactic:
hom_ext (AddMonoidHom.ext_int w)

Premises used: AddMonoidHom.ext_int, AddCommGrpCat.hom_ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G H : AddCommGrpCat
f : G ⟶ H
inst : Mono f
g₁ g₂ : (↑G : Type)
h :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₁ :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₂ :
      (↑H : Type))
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f

Tactic:
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by cat_disch
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G H : AddCommGrpCat
f : G ⟶ H
inst : Mono f
g₁ g₂ : (↑G : Type)
h :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₁ :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₂ :
      (↑H : Type))
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ asHom g₁ = asHom g₂

Tactic:
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G H : AddCommGrpCat
f : G ⟶ H
inst : Mono f
g₁ g₂ : (↑G : Type)
h :
  Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₁ :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        g₂ :
      (↑H : Type))
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂

Tactic:
apply asHom_injective t1

Premises used: AddCommGrpCat.asHom_injective
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
        (↑X : Type u_1))
      ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ (GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
        (↑Y : Type u_1))
      ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
⊢ (GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
    ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
        (↑X : Type u_1))
      ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ (CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
        (↑Y : Type u_1))
      ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
⊢ (CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Equiv.Perm α) (Iso.toEquiv 1) 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
α : Type u
⊢ ∀ (x y : Aut α), Iso.toEquiv (x * y) = Iso.toEquiv x * Iso.toEquiv y

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Aut α) (Equiv.toIso 1) 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
α : Type u
⊢ ∀ (x y : Equiv.Perm α), Equiv.toIso (x * y) = Equiv.toIso x * Equiv.toIso y

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
⊢ ∀ (x y : (↑X : Type u)), i.toEquiv.toFun (x * y) = i.toEquiv.toFun x * i.toEquiv.toFun y

Tactic:
simp [Iso.toEquiv, i]

Premises used: CategoryTheory.Iso.toEquiv
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toGrpIso.isIso_hom

Premises used: MulEquiv.toGrpIso, CategoryTheory.Iso.isIso_hom, MulEquiv.toMonoidHom
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toGrpIso.isIso_hom

Premises used: MulEquiv.toGrpIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
⊢ ∀ (x y : (↑X : Type u)), i.toEquiv.toFun (x * y) = i.toEquiv.toFun x * i.toEquiv.toFun y

Tactic:
simp [Iso.toEquiv, i]

Premises used: CategoryTheory.Iso.toEquiv
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toCommGrpIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, MulEquiv.toMonoidHom, MulEquiv.toCommGrpIso
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommGrpIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, MulEquiv.toCommGrpIso
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
⊢ HasBinaryBiproducts AddCommGrpCat

Tactic:
HasBinaryBiproducts.of_hasBinaryProducts

Premises used: CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
⊢ HasFiniteBiproducts AddCommGrpCat

Tactic:
HasFiniteBiproducts.of_hasFiniteProducts

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
G H : AddCommGrpCat
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (G.binaryProductLimitCone H).cone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj (pair G H) { as := WalkingPair.left : Discrete WalkingPair })
    ((G.binaryProductLimitCone H).cone.π.app { as := WalkingPair.left })
    (ofHom (AddMonoidHom.fst (↑G : Type u) (↑H : Type u)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
G H : AddCommGrpCat
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (G.binaryProductLimitCone H).cone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj (pair G H) { as := WalkingPair.right : Discrete WalkingPair })
    ((G.binaryProductLimitCone H).cone.π.app { as := WalkingPair.right })
    (ofHom (AddMonoidHom.snd (↑G : Type u) (↑H : Type u)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
G H : AddCommGrpCat
⊢ (G.biprodIsoProd H).inv ≫ biprod.fst = ofHom (AddMonoidHom.fst (↑G : Type u) (↑H : Type u))

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.left)

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
G H : AddCommGrpCat
⊢ (G.biprodIsoProd H).inv ≫ biprod.snd = ofHom (AddMonoidHom.snd (↑G : Type u) (↑H : Type u))

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.right)

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
G H K : AddCommGrpCat
f : G ⟶ K
g : H ⟶ K
⊢ (G.biprodIsoProd H).inv ≫ biprod.desc f g =
    HAdd.hAdd (α := of ((↑G : Type u) × (↑H : Type u)) ⟶ K) (ofHom (AddMonoidHom.fst (↑G : Type u) (↑H : Type u)) ≫ f)
      (ofHom (AddMonoidHom.snd (↑G : Type u) (↑H : Type u)) ≫ g)

Tactic:
simp [biprod.desc_eq, ← biprodIsoProd_inv_comp_fst, ← biprodIsoProd_inv_comp_snd]

Premises used: CategoryTheory.Limits.biprod.desc_eq, AddCommGrpCat.biprodIsoProd_inv_comp_snd, AddCommGrpCat.biprodIsoProd_inv_comp_fst
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type w
f : J → AddCommGrpCat
s : Fan f
simp : Eq (α := (j : J) → (↑(f j) : Type (max u w))) (fun (j : J) ↦ 0) 0
⊢ 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

Tactic:
simp only [Functor.const_obj_obj, map_zero]

Premises used: map_zero, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type w
f : J → AddCommGrpCat
s : Fan f
⊢ Eq (α := (j : J) → (↑(f j) : Type (max u w))) (fun (j : J) ↦ 0) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Biproducts
Goal:
J : Type w
f : J → AddCommGrpCat
s : Fan f
x y : (↑s.1 : Type (max u w))
⊢ (fun (j : J) ↦
      HAdd.hAdd (α := (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max u w))) (β :=
        (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max u w)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u w)) →+ (↑x2 : Type (max u w)))
                (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
                (s.π.app { as := j }) :
              (a : (↑s.pt : Type (max u w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max u w)))
            x :
          (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max u w)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u w)) →+ (↑x2 : Type (max u w)))
                (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
                (s.π.app { as := j }) :
              (a : (↑s.pt : Type (max u w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max u w)))
            y :
          (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max u w)))) =
    HAdd.hAdd (α := (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 := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
              (s.π.app { as := j : Discrete J }) :
            (a : (↑s.pt : Type (max u w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max u w)))
          x)
      fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u w)) →+ (↑x2 : Type (max u w)))
            (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
            (s.π.app { as := j : Discrete J }) :
          (a : (↑s.pt : Type (max u w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max u w)))
        y

Tactic:
rfl
-- 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
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)))
⊢ m = lift.{w, u} f s

Tactic:
ext x j