awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
A : Type u_1
inst : Monoid A
a b : A
⊢ a * b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X : MonCat
⊢ 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.MonCat.Basic
Goal:
X Y Z : MonCat
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.MonCat.Basic
Goal:
X : CommMonCat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : CommMonCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : CommMonCat
⊢ Hom.hom (𝟙 M) = MonoidHom.id (↑M : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : CommMonCat
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 M) :
        (a : (↑M : Type u_1)) → (↑M : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N T : CommMonCat
f : M ⟶ N
g : N ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N T : CommMonCat
f : M ⟶ N
g : N ⟶ T
x : (↑M : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑M : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            g :
          (a : (↑N : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                carrier) f :
              (a : (↑M : Type u_1)) → (↑N : Type u_1))
            x :
          (↑N : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : CommMonCat
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: CommMonCat.Hom.ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : Type u
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : CommMonCat
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : Type u
inst : CommMonoid M
⊢ ofHom (MonoidHom.id M) = 𝟙 (of M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N P : Type u
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
f : M →* N
g : N →* P
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : Type u
inst : CommMonoid X
inst_1 : CommMonoid Y
f : X →* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : CommMonCat
e : M ≅ N
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑N : Type u_1)) → (↑M : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) e.hom :
            (a : (↑M : Type u_1)) → (↑N : Type u_1))
          x :
        (↑N : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : CommMonCat
e : M ≅ N
s : (↑N : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑M : Type u_1)) → (↑N : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) e.inv :
            (a : (↑N : Type u_1)) → (↑M : Type u_1))
          s :
        (↑M : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
R : Type u
inst : CommMonoid R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X : CommMonCat
⊢ (↑(Functor.obj
          (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
            MonCat.carrier))
          X) :
      Type u_1) =
    (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : CommMonCat
f : X ⟶ Y
⊢ MonCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
          MonCat.carrier))
        f) =
    Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : Type u
inst : CommMonoid X
inst_1 : CommMonoid Y
f : X →* Y
⊢ CategoryTheory.Functor.map
      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      (ofHom f) =
    MonCat.ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
⊢ Functor.Full
    (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
      (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))

Tactic:
fullyFaithfulForgetToMonCat.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CommMonCat.fullyFaithfulForgetToMonCat
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X : CommMonCat
⊢ 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.MonCat.Basic
Goal:
X Y Z : CommMonCat
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.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((MonCat.Hom.hom i.inv).comp (MonCat.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))
⊢ (MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((MonCat.Hom.hom i.inv).comp (MonCat.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.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((MonCat.Hom.hom i.hom).comp (MonCat.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))
⊢ (MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((MonCat.Hom.hom i.hom).comp (MonCat.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.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((CommMonCat.Hom.hom i.inv).comp (CommMonCat.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))
⊢ (CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((CommMonCat.Hom.hom i.inv).comp (CommMonCat.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.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((CommMonCat.Hom.hom i.hom).comp (CommMonCat.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))
⊢ (CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((CommMonCat.Hom.hom i.hom).comp (CommMonCat.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.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src : OneHom (↑X : Type u) (↑Y : Type u)).toFun, invFun := __src_1.invFun, left_inv := ⋯,
    right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toMonCatIso.isIso_hom

Premises used: MulEquiv.toMonCatIso, CategoryTheory.Iso.isIso_hom, MulEquiv.toMonoidHom
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : MonCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src : OneHom (↑X : Type u) (↑Y : Type u)).toFun, invFun := __src_1.invFun, left_inv := ⋯,
    right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toMonCatIso.isIso_hom

Premises used: MulEquiv.toMonCatIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src : OneHom (↑X : Type u) (↑Y : Type u)).toFun, invFun := __src_1.invFun, left_inv := ⋯,
    right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toCommMonCatIso.isIso_hom

Premises used: MulEquiv.toCommMonCatIso, CategoryTheory.Iso.isIso_hom, MulEquiv.toMonoidHom
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src : OneHom (↑X : Type u) (↑Y : Type u)).toFun, invFun := __src_1.invFun, left_inv := ⋯,
    right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommMonCatIso.isIso_hom

Premises used: MulEquiv.toCommMonCatIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : Type u
⊢ Functor.ReflectsIsomorphisms
    (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
      CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
      MonCat.carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
⊢ Eq.{v + 1} (α := Quot (α := Prequotient F) (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop))
    (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
x y : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y) =
    HMul.hMul (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
hf :
  ∀ (x : (↑(F.obj j) : Type v)),
    Eq (α := (↑(colimit F) : Type v))
      ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
        (↑(colimit F) : Type v))
      ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
        (↑(colimit F) : Type v))
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
ext
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
hf :
  (colimitSetoid F : Prequotient F → Prequotient F → Prop)
    (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop)
    (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)

Tactic:
apply Relation.map

Premises used: MonCat.Colimits.Relation.map
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
rw :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (F.map f ≫ coconeMorphism F j') :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j) :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))

Tactic:
rw [← cocone_naturality F f]

Premises used: MonCat.Colimits.cocone_naturality
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (F.map f ≫ coconeMorphism F j') :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
f : (a : Prequotient F) → (↑s.pt : Type v)
a :
  ∀ (a b : Prequotient F) (a_1 : (colimitSetoid F : Prequotient F → Prequotient F → Prop) a b),
    descFunLift F s a = descFunLift F s b
⊢ ColimitType F → (↑s.pt : Type v)

Tactic:
fapply Quot.lift

Premises used: Quot.lift
-- Module: Mathlib.Algebra.Category.MonCat.Colimits
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
⊢ (a : Prequotient F) → (↑s.pt : Type v)

Tactic:
exact descFunLift F s

Premises used: MonCat.Colimits.descFunLift